%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO278+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 : n010.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 0.23s 5.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO278+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.47 % Computer : n010.cluster.edu
% 0.18/5.47 % Model : x86_64 x86_64
% 0.18/5.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.47 % Memory : 8046.5625MB
% 0.18/5.47 % OS : Linux 6.8.0-71-generic
% 0.18/5.47 % CPULimit : 300
% 0.18/5.47 % WCLimit : 300
% 0.18/5.47 % DateTime : Sun Sep 20 15:05:45 UTC 2026
% 0.18/5.48 % CPUTime :
% 0.23/5.52 % Drodi V4.1.1
% 0.23/5.59 % Refutation found
% 0.23/5.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/5.59 % SZS output start CNFRefutation for theBenchmark
% 0.23/5.59 fof(f1,conjecture,(
% 0.23/5.59 (! [Vdthex] :( ( ron(vd1096,Vdthex)& rcenter(vd1089,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1102 ) )),
% 0.23/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.59 fof(f2,negated_conjecture,(
% 0.23/5.59 ~((! [Vdthex] :( ( ron(vd1096,Vdthex)& rcenter(vd1089,Vdthex)& rcircle(Vdthex) )=> Vdthex = vd1102 ) ))),
% 0.23/5.59 inference(negated_conjecture,[status(cth)],[f1])).
% 0.23/5.59 fof(f3,axiom,(
% 0.23/5.59 ( ron(vd1096,vd1102)& rcenter(vd1089,vd1102)& rcircle(vd1102) ) ),
% 0.23/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.59 fof(f8,axiom,(
% 0.23/5.59 rpoint(vd1096) ),
% 0.23/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.59 fof(f41,axiom,(
% 0.23/5.59 (! [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.23/5.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/5.59 fof(f132,plain,(
% 0.23/5.59 (?[Vdthex]: (((ron(vd1096,Vdthex)&rcenter(vd1089,Vdthex))&rcircle(Vdthex))&~Vdthex=vd1102))),
% 0.23/5.59 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.23/5.59 fof(f133,plain,(
% 0.23/5.59 (((ron(vd1096,sK0_skl)&rcenter(vd1089,sK0_skl))&rcircle(sK0_skl))&~sK0_skl=vd1102)),
% 0.23/5.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f132])).
% 0.23/5.59 fof(f134,plain,(
% 0.23/5.59 ron(vd1096,sK0_skl)),
% 0.23/5.59 inference(cnf_transformation,[status(thm)],[f133])).
% 0.23/5.59 fof(f135,plain,(
% 0.23/5.59 rcenter(vd1089,sK0_skl)),
% 0.23/5.59 inference(cnf_transformation,[status(thm)],[f133])).
% 0.23/5.59 fof(f137,plain,(
% 0.23/5.59 ~sK0_skl=vd1102),
% 0.23/5.59 inference(cnf_transformation,[status(thm)],[f133])).
% 0.23/5.59 fof(f138,plain,(
% 0.23/5.59 ron(vd1096,vd1102)),
% 0.23/5.59 inference(cnf_transformation,[status(thm)],[f3])).
% 0.23/5.59 fof(f139,plain,(
% 0.23/5.59 rcenter(vd1089,vd1102)),
% 0.23/5.59 inference(cnf_transformation,[status(thm)],[f3])).
% 0.23/5.59 fof(f148,plain,(
% 0.23/5.59 rpoint(vd1096)),
% 0.23/5.59 inference(cnf_transformation,[status(thm)],[f8])).
% 0.23/5.59 fof(f234,plain,(
% 0.23/5.59 ![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.23/5.59 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.23/5.59 fof(f235,plain,(
% 0.23/5.59 ![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.23/5.59 inference(miniscoping,[status(thm)],[f234])).
% 0.23/5.59 fof(f236,plain,(
% 0.23/5.59 ![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.23/5.59 inference(cnf_transformation,[status(thm)],[f235])).
% 0.23/5.59 fof(f729,plain,(
% 0.23/5.59 ![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.23/5.59 inference(destructive_equality_resolution,[status(thm)],[f236])).
% 0.23/5.59 fof(f933,plain,(
% 0.23/5.59 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~rcenter(X3,X1)|~rcenter(X3,X2)|~rpoint(X0)|~rpoint(X0)|X2=X1)),
% 0.23/5.59 inference(equality_resolution,[status(thm)],[f729])).
% 0.23/5.59 fof(f934,plain,(
% 0.23/5.59 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~rcenter(X3,X1)|~rcenter(X3,X2)|~rpoint(X0)|X2=X1)),
% 0.23/5.59 inference(duplicate_literals_removal,[status(thm)],[f933])).
% 0.23/5.59 fof(f969,plain,(
% 0.23/5.59 ![X0,X1]: (~ron(vd1096,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|~rpoint(vd1096)|sK0_skl=X0)),
% 0.23/5.59 inference(resolution,[status(thm)],[f934,f134])).
% 0.23/5.59 fof(f987,definition,(
% 0.23/5.59 sQ20_spl <=> (rpoint(vd1096))),
% 0.23/5.59 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.23/5.59 fof(f989,plain,(
% 0.23/5.59 ~rpoint(vd1096)|sQ20_spl),
% 0.23/5.59 inference(component_clause,[status(thm)],[f987])).
% 0.23/5.59 fof(f991,definition,(
% 0.23/5.59 ![X0,X1]: (sQ21_spl <=> (~ron(vd1096,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|sK0_skl=X0))),
% 0.23/5.59 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.23/5.63 fof(f992,plain,(
% 0.23/5.63 ![X0,X1]: (~ron(vd1096,X0)|~rcenter(X1,X0)|~rcenter(X1,sK0_skl)|sK0_skl=X0|~sQ21_spl)),
% 0.23/5.63 inference(component_clause,[status(thm)],[f991])).
% 0.23/5.63 fof(f994,plain,(
% 0.23/5.63 sQ21_spl|~sQ20_spl),
% 0.23/5.63 inference(split_clause,[status(thm)],[f969,f991,f987])).
% 0.23/5.63 fof(f995,plain,(
% 0.23/5.63 $false|sQ20_spl),
% 0.23/5.63 inference(forward_subsumption_resolution,[status(thm)],[f989,f148])).
% 0.23/5.63 fof(f996,plain,(
% 0.23/5.63 sQ20_spl),
% 0.23/5.63 inference(contradiction_clause,[status(thm)],[f995])).
% 0.23/5.63 fof(f999,plain,(
% 0.23/5.63 ![X0]: (~rcenter(X0,vd1102)|~rcenter(X0,sK0_skl)|sK0_skl=vd1102|~sQ21_spl)),
% 0.23/5.63 inference(resolution,[status(thm)],[f992,f138])).
% 0.23/5.63 fof(f1001,definition,(
% 0.23/5.63 ![X0]: (sQ22_spl <=> (~rcenter(X0,vd1102)|~rcenter(X0,sK0_skl)))),
% 0.23/5.63 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.23/5.63 fof(f1002,plain,(
% 0.23/5.63 ![X0]: (~rcenter(X0,vd1102)|~rcenter(X0,sK0_skl)|~sQ22_spl)),
% 0.23/5.63 inference(component_clause,[status(thm)],[f1001])).
% 0.23/5.63 fof(f1004,definition,(
% 0.23/5.63 sQ23_spl <=> (sK0_skl=vd1102)),
% 0.23/5.63 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.23/5.63 fof(f1005,plain,(
% 0.23/5.63 sK0_skl=vd1102|~sQ23_spl),
% 0.23/5.63 inference(component_clause,[status(thm)],[f1004])).
% 0.23/5.63 fof(f1007,plain,(
% 0.23/5.63 sQ22_spl|sQ23_spl|~sQ21_spl),
% 0.23/5.63 inference(split_clause,[status(thm)],[f999,f1001,f1004,f991])).
% 0.23/5.63 fof(f1016,plain,(
% 0.23/5.63 $false|~sQ23_spl),
% 0.23/5.63 inference(forward_subsumption_resolution,[status(thm)],[f1005,f137])).
% 0.23/5.63 fof(f1017,plain,(
% 0.23/5.63 ~sQ23_spl),
% 0.23/5.63 inference(contradiction_clause,[status(thm)],[f1016])).
% 0.23/5.63 fof(f1024,plain,(
% 0.23/5.63 ~rcenter(vd1089,sK0_skl)|~sQ22_spl),
% 0.23/5.63 inference(resolution,[status(thm)],[f1002,f139])).
% 0.23/5.63 fof(f1025,plain,(
% 0.23/5.63 $false|~sQ22_spl),
% 0.23/5.63 inference(forward_subsumption_resolution,[status(thm)],[f1024,f135])).
% 0.23/5.63 fof(f1026,plain,(
% 0.23/5.63 ~sQ22_spl),
% 0.23/5.63 inference(contradiction_clause,[status(thm)],[f1025])).
% 0.23/5.63 fof(f1027,plain,(
% 0.23/5.63 $false),
% 0.23/5.63 inference(sat_refutation,[status(thm)],[f994,f996,f1007,f1017,f1026])).
% 0.23/5.63 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/5.63 % Elapsed time: 0.147035 seconds
% 0.23/5.63 % CPU time: 0.509871 seconds
% 0.23/5.63 % Total memory used: 83.938 MB
% 0.23/5.63 % Net memory used: 83.554 MB
%------------------------------------------------------------------------------