%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO272+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 : n014.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.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO272+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.35 % Computer : n014.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 14:58:50 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f1,conjecture,(
% 0.13/0.40 (! [Vdthex] :( ( ron(vd1055,Vdthex)& rcenter(vd1057,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1063 ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f2,negated_conjecture,(
% 0.13/0.40 ~((! [Vdthex] :( ( ron(vd1055,Vdthex)& rcenter(vd1057,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1063 ) ))),
% 0.13/0.40 inference(negated_conjecture,[status(cth)],[f1])).
% 0.13/0.40 fof(f3,axiom,(
% 0.13/0.40 ( ron(vd1055,vd1063)& rcenter(vd1057,vd1063)& rcircle(vd1063) ) ),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f7,axiom,(
% 0.13/0.40 ( vd1057 = vd1058& vd1055 != vd1057& rpoint(vd1058)& vd1055 = vd1056& rpoint(vd1056) ) ),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f10,axiom,(
% 0.13/0.40 (! [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.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f110,plain,(
% 0.13/0.40 (?[Vdthex]: (((ron(vd1055,Vdthex)&rcenter(vd1057,Vdthex))&rcircle(Vdthex))&~Vdthex=vd1063))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/0.40 fof(f111,plain,(
% 0.13/0.40 (((ron(vd1055,sK0_skl)&rcenter(vd1057,sK0_skl))&rcircle(sK0_skl))&~sK0_skl=vd1063)),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f110])).
% 0.13/0.40 fof(f112,plain,(
% 0.13/0.40 ron(vd1055,sK0_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f111])).
% 0.13/0.40 fof(f113,plain,(
% 0.13/0.40 rcenter(vd1057,sK0_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f111])).
% 0.13/0.40 fof(f115,plain,(
% 0.13/0.40 ~sK0_skl=vd1063),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f111])).
% 0.13/0.40 fof(f116,plain,(
% 0.13/0.40 ron(vd1055,vd1063)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.40 fof(f117,plain,(
% 0.13/0.40 rcenter(vd1057,vd1063)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.40 fof(f125,plain,(
% 0.13/0.40 vd1057=vd1058),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.40 fof(f128,plain,(
% 0.13/0.40 vd1055=vd1056),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.40 fof(f129,plain,(
% 0.13/0.40 rpoint(vd1056)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.40 fof(f140,plain,(
% 0.13/0.40 ![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.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.13/0.40 fof(f141,plain,(
% 0.13/0.40 ![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.13/0.40 inference(miniscoping,[status(thm)],[f140])).
% 0.13/0.40 fof(f142,plain,(
% 0.13/0.40 ![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.13/0.40 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.40 fof(f649,plain,(
% 0.13/0.40 ![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.13/0.40 inference(destructive_equality_resolution,[status(thm)],[f142])).
% 0.13/0.40 fof(f891,plain,(
% 0.13/0.40 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~rcenter(X3,X1)|~rcenter(X3,X2)|~rpoint(X0)|~rpoint(X0)|X2=X1)),
% 0.13/0.40 inference(equality_resolution,[status(thm)],[f649])).
% 0.13/0.40 fof(f892,plain,(
% 0.13/0.40 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~rcenter(X3,X1)|~rcenter(X3,X2)|~rpoint(X0)|X2=X1)),
% 0.13/0.40 inference(duplicate_literals_removal,[status(thm)],[f891])).
% 0.13/0.40 fof(f902,plain,(
% 0.13/0.40 rcenter(vd1058,vd1063)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f125,f117])).
% 0.13/0.40 fof(f904,plain,(
% 0.13/0.40 rcenter(vd1058,sK0_skl)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f125,f113])).
% 0.13/0.40 fof(f905,plain,(
% 0.13/0.40 ron(vd1056,vd1063)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f128,f116])).
% 0.13/0.40 fof(f906,plain,(
% 0.13/0.40 ron(vd1056,sK0_skl)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f128,f112])).
% 0.13/0.40 fof(f945,definition,(
% 0.13/0.40 sQ21_spl <=> (rpoint(vd1056))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f947,plain,(
% 0.13/0.40 ~rpoint(vd1056)|sQ21_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f945])).
% 0.13/0.40 fof(f949,plain,(
% 0.13/0.40 $false|sQ21_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f947,f129])).
% 0.13/0.40 fof(f950,plain,(
% 0.13/0.40 sQ21_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f949])).
% 0.13/0.40 fof(f991,plain,(
% 0.13/0.40 ![X0,X1]: (~ron(vd1056,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|~rpoint(vd1056)|sK0_skl=X0)),
% 0.13/0.40 inference(resolution,[status(thm)],[f892,f906])).
% 0.13/0.40 fof(f997,definition,(
% 0.13/0.40 ![X0,X1]: (sQ28_spl <=> (~ron(vd1056,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|sK0_skl=X0))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f998,plain,(
% 0.13/0.40 ![X0,X1]: (~ron(vd1056,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|sK0_skl=X0|~sQ28_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f997])).
% 0.13/0.40 fof(f1000,plain,(
% 0.13/0.40 sQ28_spl|~sQ21_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f991,f997,f945])).
% 0.13/0.40 fof(f1049,plain,(
% 0.13/0.40 ![X0]: (~rcenter(X0,vd1063)|~rcenter(X0,sK0_skl)|sK0_skl=vd1063|~sQ28_spl)),
% 0.13/0.40 inference(resolution,[status(thm)],[f998,f905])).
% 0.13/0.40 fof(f1051,definition,(
% 0.13/0.40 ![X0]: (sQ31_spl <=> (~rcenter(X0,vd1063)|~rcenter(X0,sK0_skl)))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f1052,plain,(
% 0.13/0.40 ![X0]: (~rcenter(X0,vd1063)|~rcenter(X0,sK0_skl)|~sQ31_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f1051])).
% 0.13/0.40 fof(f1054,definition,(
% 0.13/0.40 sQ32_spl <=> (sK0_skl=vd1063)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f1055,plain,(
% 0.13/0.40 sK0_skl=vd1063|~sQ32_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f1054])).
% 0.13/0.40 fof(f1057,plain,(
% 0.13/0.40 sQ31_spl|sQ32_spl|~sQ28_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f1049,f1051,f1054,f997])).
% 0.13/0.40 fof(f1072,plain,(
% 0.13/0.40 ~rcenter(vd1058,sK0_skl)|~sQ31_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f1052,f902])).
% 0.13/0.40 fof(f1073,plain,(
% 0.13/0.40 $false|~sQ31_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1072,f904])).
% 0.13/0.40 fof(f1074,plain,(
% 0.13/0.40 ~sQ31_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1073])).
% 0.13/0.40 fof(f1075,plain,(
% 0.13/0.40 $false|~sQ32_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1055,f115])).
% 0.13/0.40 fof(f1076,plain,(
% 0.13/0.40 ~sQ32_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1075])).
% 0.13/0.40 fof(f1077,plain,(
% 0.13/0.40 $false),
% 0.13/0.40 inference(sat_refutation,[status(thm)],[f950,f1000,f1057,f1074,f1076])).
% 0.13/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.44 % Elapsed time: 0.065143 seconds
% 0.13/0.44 % CPU time: 0.232378 seconds
% 0.13/0.44 % Total memory used: 118.168 MB
% 0.13/0.44 % Net memory used: 117.720 MB
%------------------------------------------------------------------------------