%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO271+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 : n008.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.11s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO271+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.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 20 15:16:40 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.41 % Drodi V4.1.1
% 0.11/0.43 % Refutation found
% 0.11/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.43 fof(f1,conjecture,(
% 0.11/0.43 (! [Vdthex] :( ( ron(vd1057,Vdthex)& rcenter(vd1055,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1061 ) )),
% 0.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.43 fof(f2,negated_conjecture,(
% 0.11/0.43 ~((! [Vdthex] :( ( ron(vd1057,Vdthex)& rcenter(vd1055,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1061 ) ))),
% 0.11/0.43 inference(negated_conjecture,[status(cth)],[f1])).
% 0.11/0.43 fof(f3,axiom,(
% 0.11/0.43 ( ron(vd1057,vd1061)& rcenter(vd1055,vd1061)& rcircle(vd1061) ) ),
% 0.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.43 fof(f4,axiom,(
% 0.11/0.43 ( vd1057 = vd1058& vd1055 != vd1057& rpoint(vd1058)& vd1055 = vd1056& rpoint(vd1056) ) ),
% 0.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.43 fof(f16,axiom,(
% 0.11/0.43 (! [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.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.43 fof(f107,plain,(
% 0.11/0.43 (?[Vdthex]: (((ron(vd1057,Vdthex)&rcenter(vd1055,Vdthex))&rcircle(Vdthex))&~Vdthex=vd1061))),
% 0.11/0.43 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.11/0.43 fof(f108,plain,(
% 0.11/0.43 (((ron(vd1057,sK0_skl)&rcenter(vd1055,sK0_skl))&rcircle(sK0_skl))&~sK0_skl=vd1061)),
% 0.11/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f107])).
% 0.11/0.43 fof(f109,plain,(
% 0.11/0.43 ron(vd1057,sK0_skl)),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f108])).
% 0.11/0.43 fof(f110,plain,(
% 0.11/0.43 rcenter(vd1055,sK0_skl)),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f108])).
% 0.11/0.43 fof(f112,plain,(
% 0.11/0.43 ~sK0_skl=vd1061),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f108])).
% 0.11/0.43 fof(f113,plain,(
% 0.11/0.43 ron(vd1057,vd1061)),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.11/0.43 fof(f114,plain,(
% 0.11/0.43 rcenter(vd1055,vd1061)),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.11/0.43 fof(f116,plain,(
% 0.11/0.43 vd1057=vd1058),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f4])).
% 0.11/0.43 fof(f118,plain,(
% 0.11/0.43 rpoint(vd1058)),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f4])).
% 0.11/0.43 fof(f119,plain,(
% 0.11/0.43 vd1055=vd1056),
% 0.11/0.43 inference(cnf_transformation,[status(thm)],[f4])).
% 0.11/0.43 fof(f174,plain,(
% 0.11/0.43 ![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.11/0.43 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.11/0.43 fof(f175,plain,(
% 0.11/0.43 ![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.11/0.43 inference(miniscoping,[status(thm)],[f174])).
% 0.11/0.43 fof(f176,plain,(
% 0.11/0.43 ![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.11/0.43 inference(cnf_transformation,[status(thm)],[f175])).
% 0.11/0.43 fof(f657,plain,(
% 0.11/0.43 ![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.11/0.43 inference(destructive_equality_resolution,[status(thm)],[f176])).
% 0.11/0.43 fof(f882,plain,(
% 0.11/0.43 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~rcenter(X3,X1)|~rcenter(X3,X2)|~rpoint(X0)|~rpoint(X0)|X2=X1)),
% 0.11/0.43 inference(equality_resolution,[status(thm)],[f657])).
% 0.11/0.43 fof(f883,plain,(
% 0.11/0.43 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~rcenter(X3,X1)|~rcenter(X3,X2)|~rpoint(X0)|X2=X1)),
% 0.11/0.43 inference(duplicate_literals_removal,[status(thm)],[f882])).
% 0.11/0.43 fof(f890,plain,(
% 0.11/0.43 ron(vd1058,vd1061)),
% 0.11/0.43 inference(backward_demodulation,[status(thm)],[f116,f113])).
% 0.11/0.43 fof(f891,plain,(
% 0.11/0.43 ron(vd1058,sK0_skl)),
% 0.11/0.43 inference(backward_demodulation,[status(thm)],[f116,f109])).
% 0.11/0.43 fof(f896,plain,(
% 0.11/0.43 rcenter(vd1056,vd1061)),
% 0.11/0.43 inference(backward_demodulation,[status(thm)],[f119,f114])).
% 0.11/0.43 fof(f897,plain,(
% 0.11/0.43 rcenter(vd1056,sK0_skl)),
% 0.11/0.43 inference(backward_demodulation,[status(thm)],[f119,f110])).
% 0.11/0.43 fof(f909,definition,(
% 0.11/0.43 sQ16_spl <=> (rpoint(vd1058))),
% 0.11/0.43 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.11/0.43 fof(f911,plain,(
% 0.11/0.43 ~rpoint(vd1058)|sQ16_spl),
% 0.11/0.43 inference(component_clause,[status(thm)],[f909])).
% 0.11/0.43 fof(f918,plain,(
% 0.11/0.43 $false|sQ16_spl),
% 0.11/0.43 inference(forward_subsumption_resolution,[status(thm)],[f911,f118])).
% 0.11/0.43 fof(f919,plain,(
% 0.11/0.43 sQ16_spl),
% 0.11/0.43 inference(contradiction_clause,[status(thm)],[f918])).
% 0.11/0.43 fof(f944,plain,(
% 0.11/0.43 ![X0,X1]: (~ron(vd1058,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|~rpoint(vd1058)|sK0_skl=X0)),
% 0.11/0.43 inference(resolution,[status(thm)],[f883,f891])).
% 0.11/0.43 fof(f946,definition,(
% 0.11/0.43 ![X0,X1]: (sQ21_spl <=> (~ron(vd1058,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|sK0_skl=X0))),
% 0.11/0.43 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.11/0.43 fof(f947,plain,(
% 0.11/0.43 ![X0,X1]: (~ron(vd1058,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|sK0_skl=X0|~sQ21_spl)),
% 0.11/0.43 inference(component_clause,[status(thm)],[f946])).
% 0.11/0.43 fof(f949,plain,(
% 0.11/0.43 sQ21_spl|~sQ16_spl),
% 0.11/0.43 inference(split_clause,[status(thm)],[f944,f946,f909])).
% 0.11/0.43 fof(f955,plain,(
% 0.11/0.43 ![X0]: (~rcenter(X0,vd1061)|~rcenter(X0,sK0_skl)|sK0_skl=vd1061|~sQ21_spl)),
% 0.11/0.43 inference(resolution,[status(thm)],[f947,f890])).
% 0.11/0.43 fof(f963,definition,(
% 0.11/0.43 ![X0]: (sQ25_spl <=> (~rcenter(X0,vd1061)|~rcenter(X0,sK0_skl)))),
% 0.11/0.43 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.11/0.43 fof(f964,plain,(
% 0.11/0.43 ![X0]: (~rcenter(X0,vd1061)|~rcenter(X0,sK0_skl)|~sQ25_spl)),
% 0.11/0.43 inference(component_clause,[status(thm)],[f963])).
% 0.11/0.43 fof(f966,definition,(
% 0.11/0.43 sQ26_spl <=> (sK0_skl=vd1061)),
% 0.11/0.43 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.11/0.43 fof(f967,plain,(
% 0.11/0.43 sK0_skl=vd1061|~sQ26_spl),
% 0.11/0.43 inference(component_clause,[status(thm)],[f966])).
% 0.11/0.43 fof(f969,plain,(
% 0.11/0.43 sQ25_spl|sQ26_spl|~sQ21_spl),
% 0.11/0.43 inference(split_clause,[status(thm)],[f955,f963,f966,f946])).
% 0.11/0.43 fof(f990,plain,(
% 0.11/0.43 ~rcenter(vd1056,sK0_skl)|~sQ25_spl),
% 0.11/0.43 inference(resolution,[status(thm)],[f964,f896])).
% 0.11/0.43 fof(f991,plain,(
% 0.11/0.43 $false|~sQ25_spl),
% 0.11/0.43 inference(forward_subsumption_resolution,[status(thm)],[f990,f897])).
% 0.11/0.43 fof(f992,plain,(
% 0.11/0.43 ~sQ25_spl),
% 0.11/0.43 inference(contradiction_clause,[status(thm)],[f991])).
% 0.11/0.43 fof(f993,plain,(
% 0.11/0.43 $false|~sQ26_spl),
% 0.11/0.43 inference(forward_subsumption_resolution,[status(thm)],[f967,f112])).
% 0.11/0.43 fof(f994,plain,(
% 0.11/0.43 ~sQ26_spl),
% 0.11/0.43 inference(contradiction_clause,[status(thm)],[f993])).
% 0.11/0.43 fof(f995,plain,(
% 0.11/0.43 $false),
% 0.11/0.43 inference(sat_refutation,[status(thm)],[f919,f949,f969,f992,f994])).
% 0.11/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.46 % Elapsed time: 0.072243 seconds
% 0.11/0.46 % CPU time: 0.191015 seconds
% 0.11/0.46 % Total memory used: 66.571 MB
% 0.11/0.46 % Net memory used: 66.299 MB
%------------------------------------------------------------------------------