%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO275+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 : n005.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:18 PM UTC 2026
% Result : Theorem 0.19s 5.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO275+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.15/5.43 % Computer : n005.cluster.edu
% 0.15/5.43 % Model : x86_64 x86_64
% 0.15/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.43 % Memory : 8046.5625MB
% 0.15/5.43 % OS : Linux 6.8.0-71-generic
% 0.15/5.43 % CPULimit : 300
% 0.15/5.43 % WCLimit : 300
% 0.15/5.43 % DateTime : Sun Sep 20 15:02:24 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.48 % Drodi V4.1.1
% 0.19/5.52 % Refutation found
% 0.19/5.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/5.52 % SZS output start CNFRefutation for theBenchmark
% 0.19/5.52 fof(f1,conjecture,(
% 0.19/5.52 (! [Vdthex] :( ( ron(vd1081,Vdthex)& rcenter(vd1080,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1095 ) )),
% 0.19/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/5.52 fof(f2,negated_conjecture,(
% 0.19/5.52 ~((! [Vdthex] :( ( ron(vd1081,Vdthex)& rcenter(vd1080,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1095 ) ))),
% 0.19/5.52 inference(negated_conjecture,[status(cth)],[f1])).
% 0.19/5.52 fof(f3,axiom,(
% 0.19/5.52 ( ron(vd1081,vd1095)& rcenter(vd1080,vd1095)& rcircle(vd1095) ) ),
% 0.19/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/5.52 fof(f8,axiom,(
% 0.19/5.52 (? [Vd1084] :( vd1081 = Vd1084& rpoint(Vd1084) ) )),
% 0.19/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/5.52 fof(f107,axiom,(
% 0.19/5.52 (! [Vd837,Vd838,Vd842,Vd843,Vd844] :( ( vf(Vd842,Vd837) = vf(Vd842,Vd838)& ron(Vd838,Vd844)& ron(Vd837,Vd843)& rcenter(Vd842,Vd844)& rcenter(Vd842,Vd843)& (? [Vd841] :( Vd838 = Vd841& rpoint(Vd841) ))& (? [Vd840] :( Vd837 = Vd840& rpoint(Vd840) ) ))=> Vd843 = Vd844 ) )),
% 0.19/5.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/5.52 fof(f122,plain,(
% 0.19/5.52 (?[Vdthex]: (((ron(vd1081,Vdthex)&rcenter(vd1080,Vdthex))&rcircle(Vdthex))&~Vdthex=vd1095))),
% 0.19/5.52 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.19/5.52 fof(f123,plain,(
% 0.19/5.52 (((ron(vd1081,sK0_skl)&rcenter(vd1080,sK0_skl))&rcircle(sK0_skl))&~sK0_skl=vd1095)),
% 0.19/5.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f122])).
% 0.19/5.52 fof(f124,plain,(
% 0.19/5.52 ron(vd1081,sK0_skl)),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f123])).
% 0.19/5.52 fof(f125,plain,(
% 0.19/5.52 rcenter(vd1080,sK0_skl)),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f123])).
% 0.19/5.52 fof(f127,plain,(
% 0.19/5.52 ~sK0_skl=vd1095),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f123])).
% 0.19/5.52 fof(f128,plain,(
% 0.19/5.52 ron(vd1081,vd1095)),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.19/5.52 fof(f129,plain,(
% 0.19/5.52 rcenter(vd1080,vd1095)),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.19/5.52 fof(f138,plain,(
% 0.19/5.52 (vd1081=sK1_skl&rpoint(sK1_skl))),
% 0.19/5.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd1084,sK1_skl)],[f8])).
% 0.19/5.52 fof(f139,plain,(
% 0.19/5.52 vd1081=sK1_skl),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f138])).
% 0.19/5.52 fof(f140,plain,(
% 0.19/5.52 rpoint(sK1_skl)),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f138])).
% 0.19/5.52 fof(f558,plain,(
% 0.19/5.52 ![Vd837,Vd838,Vd842,Vd843,Vd844]: (((((((~vf(Vd842,Vd837)=vf(Vd842,Vd838)|~ron(Vd838,Vd844))|~ron(Vd837,Vd843))|~rcenter(Vd842,Vd844))|~rcenter(Vd842,Vd843))|(![Vd841]: (~Vd838=Vd841|~rpoint(Vd841))))|(![Vd840]: (~Vd837=Vd840|~rpoint(Vd840))))|Vd843=Vd844)),
% 0.19/5.52 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 0.19/5.52 fof(f559,plain,(
% 0.19/5.52 ![Vd843,Vd844]: ((![Vd837]: ((![Vd838]: ((![Vd842]: ((((~vf(Vd842,Vd837)=vf(Vd842,Vd838)|~ron(Vd838,Vd844))|~ron(Vd837,Vd843))|~rcenter(Vd842,Vd844))|~rcenter(Vd842,Vd843)))|(![Vd841]: (~Vd838=Vd841|~rpoint(Vd841)))))|(![Vd840]: (~Vd837=Vd840|~rpoint(Vd840)))))|Vd843=Vd844)),
% 0.19/5.52 inference(miniscoping,[status(thm)],[f558])).
% 0.19/5.52 fof(f560,plain,(
% 0.19/5.52 ![X0,X1,X2,X3,X4,X5,X6]: (~vf(X0,X1)=vf(X0,X2)|~ron(X2,X3)|~ron(X1,X4)|~rcenter(X0,X3)|~rcenter(X0,X4)|~X2=X5|~rpoint(X5)|~X1=X6|~rpoint(X6)|X4=X3)),
% 0.19/5.52 inference(cnf_transformation,[status(thm)],[f559])).
% 0.19/5.52 fof(f852,plain,(
% 0.19/5.52 ![X0,X1,X2,X3,X4]: (~vf(X0,X1)=vf(X0,X2)|~ron(X2,X3)|~ron(X1,X4)|~rcenter(X0,X3)|~rcenter(X0,X4)|~rpoint(X2)|~rpoint(X1)|X4=X3)),
% 0.19/5.52 inference(destructive_equality_resolution,[status(thm)],[f560])).
% 0.19/5.52 fof(f895,plain,(
% 0.19/5.52 rpoint(vd1081)),
% 0.19/5.52 inference(forward_demodulation,[status(thm)],[f139,f140])).
% 0.19/5.52 fof(f933,definition,(
% 0.19/5.52 sQ16_spl <=> (rpoint(vd1081))),
% 0.19/5.52 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.19/5.52 fof(f935,plain,(
% 0.19/5.52 ~rpoint(vd1081)|sQ16_spl),
% 0.19/5.52 inference(component_clause,[status(thm)],[f933])).
% 0.19/5.52 fof(f944,plain,(
% 0.19/5.52 $false|sQ16_spl),
% 0.19/5.52 inference(forward_subsumption_resolution,[status(thm)],[f935,f895])).
% 0.19/5.52 fof(f945,plain,(
% 0.19/5.52 sQ16_spl),
% 0.19/5.52 inference(contradiction_clause,[status(thm)],[f944])).
% 0.19/5.52 fof(f985,plain,(
% 0.19/5.52 ![X0,X1,X2]: (~vf(X0,X1)=vf(X0,vd1081)|~ron(X1,X2)|~rcenter(X0,sK0_skl)|~rcenter(X0,X2)|~rpoint(vd1081)|~rpoint(X1)|X2=sK0_skl)),
% 0.19/5.53 inference(resolution,[status(thm)],[f852,f124])).
% 0.19/5.53 fof(f998,definition,(
% 0.19/5.53 ![X0,X1,X2]: (sQ26_spl <=> (~vf(X0,X1)=vf(X0,vd1081)|~ron(X1,X2)|~rcenter(X0,sK0_skl)|~rcenter(X0,X2)|~rpoint(X1)|X2=sK0_skl))),
% 0.19/5.53 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.19/5.53 fof(f999,plain,(
% 0.19/5.53 ![X0,X1,X2]: (~vf(X0,X1)=vf(X0,vd1081)|~ron(X1,X2)|~rcenter(X0,sK0_skl)|~rcenter(X0,X2)|~rpoint(X1)|X2=sK0_skl|~sQ26_spl)),
% 0.19/5.53 inference(component_clause,[status(thm)],[f998])).
% 0.19/5.53 fof(f1001,plain,(
% 0.19/5.53 sQ26_spl|~sQ16_spl),
% 0.19/5.53 inference(split_clause,[status(thm)],[f985,f998,f933])).
% 0.19/5.53 fof(f1076,plain,(
% 0.19/5.53 ![X0]: (~vf(X0,vd1081)=vf(X0,vd1081)|~rcenter(X0,sK0_skl)|~rcenter(X0,vd1095)|~rpoint(vd1081)|vd1095=sK0_skl|~sQ26_spl)),
% 0.19/5.53 inference(resolution,[status(thm)],[f999,f128])).
% 0.19/5.53 fof(f1089,definition,(
% 0.19/5.53 ![X0]: (sQ45_spl <=> (~vf(X0,vd1081)=vf(X0,vd1081)|~rcenter(X0,sK0_skl)|~rcenter(X0,vd1095)))),
% 0.19/5.53 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.19/5.53 fof(f1090,plain,(
% 0.19/5.53 ![X0]: (~vf(X0,vd1081)=vf(X0,vd1081)|~rcenter(X0,sK0_skl)|~rcenter(X0,vd1095)|~sQ45_spl)),
% 0.19/5.53 inference(component_clause,[status(thm)],[f1089])).
% 0.19/5.53 fof(f1092,definition,(
% 0.19/5.53 sQ46_spl <=> (vd1095=sK0_skl)),
% 0.19/5.53 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.19/5.53 fof(f1093,plain,(
% 0.19/5.53 vd1095=sK0_skl|~sQ46_spl),
% 0.19/5.53 inference(component_clause,[status(thm)],[f1092])).
% 0.19/5.53 fof(f1095,plain,(
% 0.19/5.53 sQ45_spl|~sQ16_spl|sQ46_spl|~sQ26_spl),
% 0.19/5.53 inference(split_clause,[status(thm)],[f1076,f1089,f933,f1092,f998])).
% 0.19/5.53 fof(f1103,plain,(
% 0.19/5.53 ![X0]: (~rcenter(X0,sK0_skl)|~rcenter(X0,vd1095)|~sQ45_spl)),
% 0.19/5.53 inference(trivial_equality_resolution,[status(thm)],[f1090])).
% 0.19/5.53 fof(f1177,plain,(
% 0.19/5.53 ~rcenter(vd1080,vd1095)|~sQ45_spl),
% 0.19/5.53 inference(resolution,[status(thm)],[f1103,f125])).
% 0.19/5.53 fof(f1178,plain,(
% 0.19/5.53 $false|~sQ45_spl),
% 0.19/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1177,f129])).
% 0.19/5.53 fof(f1179,plain,(
% 0.19/5.53 ~sQ45_spl),
% 0.19/5.53 inference(contradiction_clause,[status(thm)],[f1178])).
% 0.19/5.53 fof(f1180,plain,(
% 0.19/5.53 $false|~sQ46_spl),
% 0.19/5.53 inference(forward_subsumption_resolution,[status(thm)],[f1093,f127])).
% 0.19/5.53 fof(f1181,plain,(
% 0.19/5.53 ~sQ46_spl),
% 0.19/5.53 inference(contradiction_clause,[status(thm)],[f1180])).
% 0.19/5.53 fof(f1182,plain,(
% 0.19/5.53 $false),
% 0.19/5.53 inference(sat_refutation,[status(thm)],[f945,f1001,f1095,f1179,f1181])).
% 0.19/5.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/5.58 % Elapsed time: 0.136209 seconds
% 0.19/5.58 % CPU time: 0.321124 seconds
% 0.19/5.58 % Total memory used: 52.888 MB
% 0.19/5.58 % Net memory used: 52.664 MB
%------------------------------------------------------------------------------