%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO284+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 : 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 9.39s 1.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO284+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.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 15:08:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 9.39/1.68 % Refutation found
% 9.39/1.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.39/1.68 % SZS output start CNFRefutation for theBenchmark
% 9.39/1.68 fof(f1,conjecture,(
% 9.39/1.68 (? [Vd1151,Vd1152] :( ron(vd1127,Vd1152)& rcenter(vd1123,Vd1152)& rcircle(Vd1152)& ron(vd1125,Vd1151)& ron(vd1123,Vd1151)& rline(Vd1151) ) )),
% 9.39/1.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.39/1.68 fof(f2,negated_conjecture,(
% 9.39/1.68 ~((? [Vd1151,Vd1152] :( ron(vd1127,Vd1152)& rcenter(vd1123,Vd1152)& rcircle(Vd1152)& ron(vd1125,Vd1151)& ron(vd1123,Vd1151)& rline(Vd1151) ) ))),
% 9.39/1.68 inference(negated_conjecture,[status(cth)],[f1])).
% 9.39/1.68 fof(f3,axiom,(
% 9.39/1.68 vd1123 = vd1129 ),
% 9.39/1.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.39/1.68 fof(f13,axiom,(
% 9.39/1.68 ( 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) ) ),
% 9.39/1.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.39/1.68 fof(f20,axiom,(
% 9.39/1.68 (! [Vd225,Vd226] :( ( Vd225 != Vd226& (? [Vd230] :( Vd226 = Vd230& rpoint(Vd230) ))& (? [Vd229] :( Vd225 = Vd229& rpoint(Vd229) ) ))=> (? [Vd231] :( ron(Vd226,Vd231)& rcenter(Vd225,Vd231)& rcircle(Vd231) ) )) )),
% 9.39/1.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.39/1.68 fof(f34,axiom,(
% 9.39/1.68 (! [Vd217,Vd218] :( ( Vd217 != Vd218& (? [Vd221] :( Vd218 = Vd221& rpoint(Vd221) ))& (? [Vd220] :( Vd217 = Vd220& rpoint(Vd220) ) ))=> (? [Vd223] :( ron(Vd218,Vd223)& ron(Vd217,Vd223)& rline(Vd223) ) )) )),
% 9.39/1.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.39/1.68 fof(f133,plain,(
% 9.39/1.68 (![Vd1151,Vd1152]: (((((~ron(vd1127,Vd1152)|~rcenter(vd1123,Vd1152))|~rcircle(Vd1152))|~ron(vd1125,Vd1151))|~ron(vd1123,Vd1151))|~rline(Vd1151)))),
% 9.39/1.68 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 9.39/1.68 fof(f134,plain,(
% 9.39/1.68 ![Vd1151]: ((((![Vd1152]: ((~ron(vd1127,Vd1152)|~rcenter(vd1123,Vd1152))|~rcircle(Vd1152)))|~ron(vd1125,Vd1151))|~ron(vd1123,Vd1151))|~rline(Vd1151))),
% 9.39/1.68 inference(miniscoping,[status(thm)],[f133])).
% 9.39/1.68 fof(f135,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1127,X0)|~rcenter(vd1123,X0)|~rcircle(X0)|~ron(vd1125,X1)|~ron(vd1123,X1)|~rline(X1))),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f134])).
% 9.39/1.68 fof(f136,plain,(
% 9.39/1.68 vd1123=vd1129),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f3])).
% 9.39/1.68 fof(f160,plain,(
% 9.39/1.68 ~vd1127=vd1129),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f161,plain,(
% 9.39/1.68 ~vd1123=vd1125),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f162,plain,(
% 9.39/1.68 vd1129=vd1130),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f163,plain,(
% 9.39/1.68 rpoint(vd1130)),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f164,plain,(
% 9.39/1.68 vd1127=vd1128),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f165,plain,(
% 9.39/1.68 rpoint(vd1128)),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f166,plain,(
% 9.39/1.68 vd1125=vd1126),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f167,plain,(
% 9.39/1.68 rpoint(vd1126)),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f13])).
% 9.39/1.68 fof(f199,plain,(
% 9.39/1.68 ![Vd225,Vd226]: (((Vd225=Vd226|(![Vd230]: (~Vd226=Vd230|~rpoint(Vd230))))|(![Vd229]: (~Vd225=Vd229|~rpoint(Vd229))))|(?[Vd231]: ((ron(Vd226,Vd231)&rcenter(Vd225,Vd231))&rcircle(Vd231))))),
% 9.39/1.68 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 9.39/1.68 fof(f200,plain,(
% 9.39/1.68 ![Vd225,Vd226]: (((Vd225=Vd226|(![Vd230]: (~Vd226=Vd230|~rpoint(Vd230))))|(![Vd229]: (~Vd225=Vd229|~rpoint(Vd229))))|((ron(Vd226,sK2_skl(Vd226,Vd225))&rcenter(Vd225,sK2_skl(Vd226,Vd225)))&rcircle(sK2_skl(Vd226,Vd225))))),
% 9.39/1.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd231,sK2_skl(Vd226,Vd225))],[f199])).
% 9.39/1.68 fof(f201,plain,(
% 9.39/1.68 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|ron(X1,sK2_skl(X1,X0)))),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f200])).
% 9.39/1.68 fof(f202,plain,(
% 9.39/1.68 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|rcenter(X0,sK2_skl(X1,X0)))),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f200])).
% 9.39/1.68 fof(f203,plain,(
% 9.39/1.68 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|rcircle(sK2_skl(X1,X0)))),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f200])).
% 9.39/1.68 fof(f239,plain,(
% 9.39/1.68 ![Vd217,Vd218]: (((Vd217=Vd218|(![Vd221]: (~Vd218=Vd221|~rpoint(Vd221))))|(![Vd220]: (~Vd217=Vd220|~rpoint(Vd220))))|(?[Vd223]: ((ron(Vd218,Vd223)&ron(Vd217,Vd223))&rline(Vd223))))),
% 9.39/1.68 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 9.39/1.68 fof(f240,plain,(
% 9.39/1.68 ![Vd217,Vd218]: (((Vd217=Vd218|(![Vd221]: (~Vd218=Vd221|~rpoint(Vd221))))|(![Vd220]: (~Vd217=Vd220|~rpoint(Vd220))))|((ron(Vd218,sK4_skl(Vd218,Vd217))&ron(Vd217,sK4_skl(Vd218,Vd217)))&rline(sK4_skl(Vd218,Vd217))))),
% 9.39/1.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Vd223,sK4_skl(Vd218,Vd217))],[f239])).
% 9.39/1.68 fof(f241,plain,(
% 9.39/1.68 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|ron(X1,sK4_skl(X1,X0)))),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f240])).
% 9.39/1.68 fof(f242,plain,(
% 9.39/1.68 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|ron(X0,sK4_skl(X1,X0)))),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f240])).
% 9.39/1.68 fof(f243,plain,(
% 9.39/1.68 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|rline(sK4_skl(X1,X0)))),
% 9.39/1.68 inference(cnf_transformation,[status(thm)],[f240])).
% 9.39/1.68 fof(f708,plain,(
% 9.39/1.68 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|ron(X1,sK2_skl(X1,X0)))),
% 9.39/1.68 inference(destructive_equality_resolution,[status(thm)],[f201])).
% 9.39/1.68 fof(f709,plain,(
% 9.39/1.68 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|rcenter(X0,sK2_skl(X1,X0)))),
% 9.39/1.68 inference(destructive_equality_resolution,[status(thm)],[f202])).
% 9.39/1.68 fof(f710,plain,(
% 9.39/1.68 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|rcircle(sK2_skl(X1,X0)))),
% 9.39/1.68 inference(destructive_equality_resolution,[status(thm)],[f203])).
% 9.39/1.68 fof(f715,plain,(
% 9.39/1.68 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|ron(X1,sK4_skl(X1,X0)))),
% 9.39/1.68 inference(destructive_equality_resolution,[status(thm)],[f241])).
% 9.39/1.68 fof(f716,plain,(
% 9.39/1.68 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|ron(X0,sK4_skl(X1,X0)))),
% 9.39/1.68 inference(destructive_equality_resolution,[status(thm)],[f242])).
% 9.39/1.68 fof(f717,plain,(
% 9.39/1.68 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|rline(sK4_skl(X1,X0)))),
% 9.39/1.68 inference(destructive_equality_resolution,[status(thm)],[f243])).
% 9.39/1.68 fof(f907,plain,(
% 9.39/1.68 ~vd1129=vd1125),
% 9.39/1.68 inference(backward_demodulation,[status(thm)],[f136,f161])).
% 9.39/1.68 fof(f909,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1127,X0)|~rcenter(vd1123,X0)|~rcircle(X0)|~ron(vd1125,X1)|~ron(vd1129,X1)|~rline(X1))),
% 9.39/1.68 inference(backward_demodulation,[status(thm)],[f136,f135])).
% 9.39/1.68 fof(f910,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1127,X0)|~rcenter(vd1129,X0)|~rcircle(X0)|~ron(vd1125,X1)|~ron(vd1129,X1)|~rline(X1))),
% 9.39/1.68 inference(forward_demodulation,[status(thm)],[f136,f909])).
% 9.39/1.68 fof(f1197,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1128,X0)|~rcenter(vd1129,X0)|~rcircle(X0)|~ron(vd1125,X1)|~ron(vd1129,X1)|~rline(X1))),
% 9.39/1.68 inference(forward_demodulation,[status(thm)],[f164,f910])).
% 9.39/1.68 fof(f1198,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1128,X0)|~rcenter(vd1130,X0)|~rcircle(X0)|~ron(vd1125,X1)|~ron(vd1129,X1)|~rline(X1))),
% 9.39/1.68 inference(forward_demodulation,[status(thm)],[f162,f1197])).
% 9.39/1.68 fof(f1199,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1128,X0)|~rcenter(vd1130,X0)|~rcircle(X0)|~ron(vd1126,X1)|~ron(vd1129,X1)|~rline(X1))),
% 9.39/1.68 inference(forward_demodulation,[status(thm)],[f166,f1198])).
% 9.39/1.68 fof(f1200,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1128,X0)|~rcenter(vd1130,X0)|~rcircle(X0)|~ron(vd1126,X1)|~ron(vd1130,X1)|~rline(X1))),
% 9.39/1.68 inference(forward_demodulation,[status(thm)],[f162,f1199])).
% 9.39/1.68 fof(f1201,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1128,sK2_skl(X0,vd1130))|~rcircle(sK2_skl(X0,vd1130))|~ron(vd1126,X1)|~ron(vd1130,X1)|~rline(X1)|vd1130=X0|~rpoint(X0)|~rpoint(vd1130))),
% 9.39/1.68 inference(resolution,[status(thm)],[f1200,f709])).
% 9.39/1.68 fof(f1202,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1128,sK2_skl(X0,vd1130))|~ron(vd1126,X1)|~ron(vd1130,X1)|~rline(X1)|vd1130=X0|~rpoint(X0)|~rpoint(vd1130))),
% 9.39/1.68 inference(forward_subsumption_resolution,[status(thm)],[f1201,f710])).
% 9.39/1.68 fof(f1203,plain,(
% 9.39/1.68 ![X0,X1]: (~ron(vd1128,sK2_skl(X0,vd1130))|~ron(vd1126,X1)|~ron(vd1130,X1)|~rline(X1)|vd1130=X0|~rpoint(X0))),
% 9.39/1.68 inference(forward_subsumption_resolution,[status(thm)],[f1202,f163])).
% 9.39/1.68 fof(f1204,plain,(
% 9.39/1.68 ![X0,X1,X2]: (~ron(vd1128,sK2_skl(X0,vd1130))|~ron(vd1126,sK4_skl(X1,X2))|~ron(vd1130,sK4_skl(X1,X2))|vd1130=X0|~rpoint(X0)|X2=X1|~rpoint(X1)|~rpoint(X2))),
% 9.39/1.68 inference(resolution,[status(thm)],[f1203,f717])).
% 9.39/1.69 fof(f1207,plain,(
% 9.39/1.69 ~vd1130=vd1125),
% 9.39/1.69 inference(forward_demodulation,[status(thm)],[f162,f907])).
% 9.39/1.69 fof(f1209,plain,(
% 9.39/1.69 ~vd1130=vd1126),
% 9.39/1.69 inference(forward_demodulation,[status(thm)],[f166,f1207])).
% 9.39/1.69 fof(f1365,plain,(
% 9.39/1.69 ![X0,X1]: (~ron(vd1126,sK4_skl(X0,X1))|~ron(vd1130,sK4_skl(X0,X1))|vd1130=vd1128|~rpoint(vd1128)|X1=X0|~rpoint(X0)|~rpoint(X1)|vd1130=vd1128|~rpoint(vd1128)|~rpoint(vd1130))),
% 9.39/1.69 inference(resolution,[status(thm)],[f1204,f708])).
% 9.39/1.69 fof(f1369,plain,(
% 9.39/1.69 ![X0,X1]: (~ron(vd1126,sK4_skl(X0,X1))|~ron(vd1130,sK4_skl(X0,X1))|vd1130=vd1128|~rpoint(vd1128)|X1=X0|~rpoint(X0)|~rpoint(X1)|~rpoint(vd1130))),
% 9.39/1.69 inference(duplicate_literals_removal,[status(thm)],[f1365])).
% 9.39/1.69 fof(f1370,plain,(
% 9.39/1.69 ![X0,X1]: (~ron(vd1126,sK4_skl(X0,X1))|~ron(vd1130,sK4_skl(X0,X1))|vd1130=vd1128|X1=X0|~rpoint(X0)|~rpoint(X1)|~rpoint(vd1130))),
% 9.39/1.69 inference(forward_subsumption_resolution,[status(thm)],[f1369,f165])).
% 9.39/1.69 fof(f1371,plain,(
% 9.39/1.69 ![X0,X1]: (~ron(vd1126,sK4_skl(X0,X1))|~ron(vd1130,sK4_skl(X0,X1))|vd1130=vd1128|X1=X0|~rpoint(X0)|~rpoint(X1))),
% 9.39/1.69 inference(forward_subsumption_resolution,[status(thm)],[f1370,f163])).
% 9.39/1.69 fof(f1372,plain,(
% 9.39/1.69 ![X0]: (~ron(vd1130,sK4_skl(X0,vd1126))|vd1130=vd1128|vd1126=X0|~rpoint(X0)|~rpoint(vd1126)|vd1126=X0|~rpoint(X0)|~rpoint(vd1126))),
% 9.39/1.69 inference(resolution,[status(thm)],[f1371,f716])).
% 9.39/1.69 fof(f1377,plain,(
% 9.39/1.69 ![X0]: (~ron(vd1130,sK4_skl(X0,vd1126))|vd1130=vd1128|vd1126=X0|~rpoint(X0)|~rpoint(vd1126))),
% 9.39/1.69 inference(duplicate_literals_removal,[status(thm)],[f1372])).
% 9.39/1.69 fof(f1378,plain,(
% 9.39/1.69 ![X0]: (~ron(vd1130,sK4_skl(X0,vd1126))|vd1130=vd1128|vd1126=X0|~rpoint(X0))),
% 9.39/1.69 inference(forward_subsumption_resolution,[status(thm)],[f1377,f167])).
% 9.39/1.69 fof(f1382,plain,(
% 9.39/1.69 vd1130=vd1128|vd1126=vd1130|~rpoint(vd1130)|vd1126=vd1130|~rpoint(vd1130)|~rpoint(vd1126)),
% 9.39/1.69 inference(resolution,[status(thm)],[f1378,f715])).
% 9.39/1.69 fof(f1386,plain,(
% 9.39/1.69 vd1130=vd1128|vd1126=vd1130|~rpoint(vd1130)|~rpoint(vd1126)),
% 9.39/1.69 inference(duplicate_literals_removal,[status(thm)],[f1382])).
% 9.39/1.69 fof(f1387,plain,(
% 9.39/1.69 vd1130=vd1128|~rpoint(vd1130)|~rpoint(vd1126)),
% 9.39/1.69 inference(forward_subsumption_resolution,[status(thm)],[f1386,f1209])).
% 9.39/1.69 fof(f1573,plain,(
% 9.39/1.69 vd1130=vd1128|~rpoint(vd1126)),
% 9.39/1.69 inference(forward_subsumption_resolution,[status(thm)],[f1387,f163])).
% 9.39/1.69 fof(f1574,plain,(
% 9.39/1.69 vd1130=vd1128),
% 9.39/1.69 inference(resolution,[status(thm)],[f1573,f167])).
% 9.39/1.69 fof(f1606,plain,(
% 9.39/1.69 vd1127=vd1130),
% 9.39/1.69 inference(backward_demodulation,[status(thm)],[f1574,f164])).
% 9.39/1.69 fof(f2564,plain,(
% 9.39/1.69 ~vd1130=vd1129),
% 9.39/1.69 inference(forward_demodulation,[status(thm)],[f1606,f160])).
% 9.39/1.69 fof(f2565,plain,(
% 9.39/1.69 ~vd1130=vd1130),
% 9.39/1.69 inference(forward_demodulation,[status(thm)],[f162,f2564])).
% 9.39/1.69 fof(f2566,plain,(
% 9.39/1.69 $false),
% 9.39/1.69 inference(trivial_equality_resolution,[status(thm)],[f2565])).
% 9.39/1.69 % SZS output end CNFRefutation for theBenchmark.p
% 0.45/1.72 % Elapsed time: 1.337058 seconds
% 0.45/1.72 % CPU time: 10.133867 seconds
% 0.45/1.72 % Total memory used: 189.622 MB
% 0.45/1.72 % Net memory used: 181.823 MB
%------------------------------------------------------------------------------