%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO300+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 : n011.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:20 PM UTC 2026
% Result : Theorem 0.10s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO300+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.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 15:14:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 0.10/0.43 % Refutation found
% 0.10/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.43 fof(f1,conjecture,(
% 0.10/0.43 vf(vd1185,vd1201) = vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)) ),
% 0.10/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.43 fof(f2,negated_conjecture,(
% 0.10/0.43 ~(vf(vd1185,vd1201) = vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)) )),
% 0.10/0.43 inference(negated_conjecture,[status(cth)],[f1])).
% 0.10/0.43 fof(f3,axiom,(
% 0.10/0.43 rR(vd1187,vd1185,vd1201) ),
% 0.10/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.43 fof(f6,axiom,(
% 0.10/0.43 (! [Vd828,Vd829,Vd830] :( ( rR(Vd829,Vd828,Vd830)& (? [Vd834] :( Vd830 = Vd834& rpoint(Vd834) ))& (? [Vd833] :( Vd829 = Vd833& rpoint(Vd833) ))& (? [Vd832] :( Vd828 = Vd832& rpoint(Vd832) ) ))=> vplus(vf(Vd828,Vd829),vf(Vd829,Vd830)) = vf(Vd828,Vd830) ) )),
% 0.10/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.43 fof(f8,axiom,(
% 0.10/0.43 (? [Vd1205] :( vd1201 = Vd1205& rpoint(Vd1205) ) )),
% 0.10/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.43 fof(f9,axiom,(
% 0.10/0.43 ( ~ (? [Vd1195] :( ron(vd1187,Vd1195)& ron(vd1186,Vd1195)& ron(vd1185,Vd1195)& rline(Vd1195) ))& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)& vf(vd1178,vd1180) = vf(vd1185,vd1187)& vf(vd1178,vd1179) = vf(vd1185,vd1186)& (? [Vd1191] :( vd1187 = Vd1191& rpoint(Vd1191) ))& (? [Vd1190] :( vd1186 = Vd1190& rpoint(Vd1190) ))& (? [Vd1189] :( vd1185 = Vd1189& rpoint(Vd1189) ))& vd1179 != vd1180& vd1178 != vd1180& vd1178 != vd1179& (? [Vd1184] :( vd1180 = Vd1184& rpoint(Vd1184) ))& (? [Vd1183] :( vd1179 = Vd1183& rpoint(Vd1183) ))& (? [Vd1182] :( vd1178 = Vd1182& rpoint(Vd1182) ) )) ),
% 0.10/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.43 fof(f163,plain,(
% 0.10/0.43 ~vf(vd1185,vd1201)=vplus(vf(vd1185,vd1187),vf(vd1187,vd1201))),
% 0.10/0.43 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.43 fof(f164,plain,(
% 0.10/0.43 rR(vd1187,vd1185,vd1201)),
% 0.10/0.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.43 fof(f167,plain,(
% 0.10/0.43 ![Vd828,Vd829,Vd830]: ((((~rR(Vd829,Vd828,Vd830)|(![Vd834]: (~Vd830=Vd834|~rpoint(Vd834))))|(![Vd833]: (~Vd829=Vd833|~rpoint(Vd833))))|(![Vd832]: (~Vd828=Vd832|~rpoint(Vd832))))|vplus(vf(Vd828,Vd829),vf(Vd829,Vd830))=vf(Vd828,Vd830))),
% 0.10/0.43 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.10/0.43 fof(f168,plain,(
% 0.10/0.43 ![X0,X1,X2,X3,X4,X5]: (~rR(X0,X1,X2)|~X2=X3|~rpoint(X3)|~X0=X4|~rpoint(X4)|~X1=X5|~rpoint(X5)|vplus(vf(X1,X0),vf(X0,X2))=vf(X1,X2))),
% 0.10/0.43 inference(cnf_transformation,[status(thm)],[f167])).
% 0.10/0.43 fof(f170,plain,(
% 0.10/0.43 (vd1201=sK0_skl&rpoint(sK0_skl))),
% 0.10/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1205,sK0_skl)],[f8])).
% 0.10/0.43 fof(f171,plain,(
% 0.10/0.43 vd1201=sK0_skl),
% 0.10/0.43 inference(cnf_transformation,[status(thm)],[f170])).
% 0.10/0.43 fof(f172,plain,(
% 0.10/0.43 rpoint(sK0_skl)),
% 0.10/0.43 inference(cnf_transformation,[status(thm)],[f170])).
% 0.10/0.43 fof(f173,plain,(
% 0.10/0.43 ((((((((((((![Vd1195]: (((~ron(vd1187,Vd1195)|~ron(vd1186,Vd1195))|~ron(vd1185,Vd1195))|~rline(Vd1195)))&vangle(vd1179,vd1178,vd1180)=vangle(vd1186,vd1185,vd1187))&vf(vd1178,vd1180)=vf(vd1185,vd1187))&vf(vd1178,vd1179)=vf(vd1185,vd1186))&(?[Vd1191]: (vd1187=Vd1191&rpoint(Vd1191))))&(?[Vd1190]: (vd1186=Vd1190&rpoint(Vd1190))))&(?[Vd1189]: (vd1185=Vd1189&rpoint(Vd1189))))&~vd1179=vd1180)&~vd1178=vd1180)&~vd1178=vd1179)&(?[Vd1184]: (vd1180=Vd1184&rpoint(Vd1184))))&(?[Vd1183]: (vd1179=Vd1183&rpoint(Vd1183))))&(?[Vd1182]: (vd1178=Vd1182&rpoint(Vd1182)))),
% 0.10/0.43 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.10/0.43 fof(f174,plain,(
% 0.10/0.43 ((((((((((((![Vd1195]: (((~ron(vd1187,Vd1195)|~ron(vd1186,Vd1195))|~ron(vd1185,Vd1195))|~rline(Vd1195)))&vangle(vd1179,vd1178,vd1180)=vangle(vd1186,vd1185,vd1187))&vf(vd1178,vd1180)=vf(vd1185,vd1187))&vf(vd1178,vd1179)=vf(vd1185,vd1186))&(vd1187=sK1_skl&rpoint(sK1_skl)))&(vd1186=sK2_skl&rpoint(sK2_skl)))&(vd1185=sK3_skl&rpoint(sK3_skl)))&~vd1179=vd1180)&~vd1178=vd1180)&~vd1178=vd1179)&(vd1180=sK4_skl&rpoint(sK4_skl)))&(vd1179=sK5_skl&rpoint(sK5_skl)))&(vd1178=sK6_skl&rpoint(sK6_skl))),
% 0.10/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(Vd1191,sK1_skl),skolemize(Vd1190,sK2_skl),skolemize(Vd1189,sK3_skl),skolemize(Vd1184,sK4_skl),skolemize(Vd1183,sK5_skl),skolemize(Vd1182,sK6_skl)],[f173])).
% 0.10/0.44 fof(f179,plain,(
% 0.10/0.44 vd1187=sK1_skl),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f174])).
% 0.10/0.44 fof(f180,plain,(
% 0.10/0.44 rpoint(sK1_skl)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f174])).
% 0.10/0.44 fof(f183,plain,(
% 0.10/0.44 vd1185=sK3_skl),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f174])).
% 0.10/0.44 fof(f184,plain,(
% 0.10/0.44 rpoint(sK3_skl)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f174])).
% 0.10/0.44 fof(f809,plain,(
% 0.10/0.44 ![X0,X1,X2]: (~rR(X0,X1,X2)|~rpoint(X2)|~rpoint(X0)|~rpoint(X1)|vplus(vf(X1,X0),vf(X0,X2))=vf(X1,X2))),
% 0.10/0.44 inference(destructive_equality_resolution,[status(thm)],[f168])).
% 0.10/0.44 fof(f1030,plain,(
% 0.10/0.44 ~rpoint(vd1201)|~rpoint(vd1187)|~rpoint(vd1185)|vplus(vf(vd1185,vd1187),vf(vd1187,vd1201))=vf(vd1185,vd1201)),
% 0.10/0.44 inference(resolution,[status(thm)],[f809,f164])).
% 0.10/0.44 fof(f1031,definition,(
% 0.10/0.44 sQ16_spl <=> (rpoint(vd1201))),
% 0.10/0.44 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.10/0.44 fof(f1033,plain,(
% 0.10/0.44 ~rpoint(vd1201)|sQ16_spl),
% 0.10/0.44 inference(component_clause,[status(thm)],[f1031])).
% 0.10/0.44 fof(f1034,definition,(
% 0.10/0.44 sQ17_spl <=> (rpoint(vd1187))),
% 0.10/0.44 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.10/0.44 fof(f1036,plain,(
% 0.10/0.44 ~rpoint(vd1187)|sQ17_spl),
% 0.10/0.44 inference(component_clause,[status(thm)],[f1034])).
% 0.10/0.44 fof(f1037,definition,(
% 0.10/0.44 sQ18_spl <=> (rpoint(vd1185))),
% 0.10/0.44 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.10/0.44 fof(f1039,plain,(
% 0.10/0.44 ~rpoint(vd1185)|sQ18_spl),
% 0.10/0.44 inference(component_clause,[status(thm)],[f1037])).
% 0.10/0.44 fof(f1040,definition,(
% 0.10/0.44 sQ19_spl <=> (vplus(vf(vd1185,vd1187),vf(vd1187,vd1201))=vf(vd1185,vd1201))),
% 0.10/0.44 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.44 fof(f1041,plain,(
% 0.10/0.44 vplus(vf(vd1185,vd1187),vf(vd1187,vd1201))=vf(vd1185,vd1201)|~sQ19_spl),
% 0.10/0.44 inference(component_clause,[status(thm)],[f1040])).
% 0.10/0.44 fof(f1043,plain,(
% 0.10/0.44 ~sQ16_spl|~sQ17_spl|~sQ18_spl|sQ19_spl),
% 0.10/0.44 inference(split_clause,[status(thm)],[f1030,f1031,f1034,f1037,f1040])).
% 0.10/0.44 fof(f1044,plain,(
% 0.10/0.44 $false|~sQ19_spl),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1041,f163])).
% 0.10/0.44 fof(f1045,plain,(
% 0.10/0.44 ~sQ19_spl),
% 0.10/0.44 inference(contradiction_clause,[status(thm)],[f1044])).
% 0.10/0.44 fof(f1068,plain,(
% 0.10/0.44 ~rpoint(sK3_skl)|sQ18_spl),
% 0.10/0.44 inference(backward_demodulation,[status(thm)],[f183,f1039])).
% 0.10/0.44 fof(f1086,plain,(
% 0.10/0.44 $false|sQ18_spl),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1068,f184])).
% 0.10/0.44 fof(f1087,plain,(
% 0.10/0.44 sQ18_spl),
% 0.10/0.44 inference(contradiction_clause,[status(thm)],[f1086])).
% 0.10/0.44 fof(f1088,plain,(
% 0.10/0.44 ~rpoint(sK0_skl)|sQ16_spl),
% 0.10/0.44 inference(forward_demodulation,[status(thm)],[f171,f1033])).
% 0.10/0.44 fof(f1089,plain,(
% 0.10/0.44 $false|sQ16_spl),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1088,f172])).
% 0.10/0.44 fof(f1090,plain,(
% 0.10/0.44 sQ16_spl),
% 0.10/0.44 inference(contradiction_clause,[status(thm)],[f1089])).
% 0.10/0.44 fof(f1092,plain,(
% 0.10/0.44 ~rpoint(sK1_skl)|sQ17_spl),
% 0.10/0.44 inference(forward_demodulation,[status(thm)],[f179,f1036])).
% 0.10/0.44 fof(f1093,plain,(
% 0.10/0.44 $false|sQ17_spl),
% 0.10/0.44 inference(forward_subsumption_resolution,[status(thm)],[f1092,f180])).
% 0.10/0.44 fof(f1094,plain,(
% 0.10/0.44 sQ17_spl),
% 0.10/0.44 inference(contradiction_clause,[status(thm)],[f1093])).
% 0.10/0.44 fof(f1095,plain,(
% 0.10/0.44 $false),
% 0.10/0.44 inference(sat_refutation,[status(thm)],[f1043,f1045,f1087,f1090,f1094])).
% 0.10/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.46 % Elapsed time: 0.075536 seconds
% 0.10/0.46 % CPU time: 0.239147 seconds
% 0.10/0.46 % Total memory used: 121.184 MB
% 0.10/0.46 % Net memory used: 120.722 MB
%------------------------------------------------------------------------------