%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO299+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 : 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:20 PM UTC 2026
% Result : Theorem 0.16s 5.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO299+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n008.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sun Sep 20 15:16:59 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.16/5.42 % Drodi V4.1.1
% 0.16/5.45 % Refutation found
% 0.16/5.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/5.45 % SZS output start CNFRefutation for theBenchmark
% 0.16/5.45 fof(f1,conjecture,(
% 0.16/5.45 vf(vd1185,vd1187) = vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)) ),
% 0.16/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f2,negated_conjecture,(
% 0.16/5.45 ~(vf(vd1185,vd1187) = vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)) )),
% 0.16/5.45 inference(negated_conjecture,[status(cth)],[f1])).
% 0.16/5.45 fof(f3,axiom,(
% 0.16/5.45 rR(vd1201,vd1185,vd1187) ),
% 0.16/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f8,axiom,(
% 0.16/5.45 (! [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.16/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f22,axiom,(
% 0.16/5.45 (? [Vd1205] :( vd1201 = Vd1205& rpoint(Vd1205) ) )),
% 0.16/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f26,axiom,(
% 0.16/5.45 ( ~ (? [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.16/5.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/5.45 fof(f162,plain,(
% 0.16/5.45 ~vf(vd1185,vd1187)=vplus(vf(vd1185,vd1201),vf(vd1201,vd1187))),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/5.45 fof(f163,plain,(
% 0.16/5.45 rR(vd1201,vd1185,vd1187)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.16/5.45 fof(f168,plain,(
% 0.16/5.45 ![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.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.16/5.45 fof(f169,plain,(
% 0.16/5.45 ![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.16/5.45 inference(cnf_transformation,[status(thm)],[f168])).
% 0.16/5.45 fof(f188,plain,(
% 0.16/5.45 (vd1201=sK0_skl&rpoint(sK0_skl))),
% 0.16/5.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1205,sK0_skl)],[f22])).
% 0.16/5.45 fof(f189,plain,(
% 0.16/5.45 vd1201=sK0_skl),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f188])).
% 0.16/5.45 fof(f190,plain,(
% 0.16/5.45 rpoint(sK0_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f188])).
% 0.16/5.45 fof(f196,plain,(
% 0.16/5.45 ((((((((((((![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.16/5.45 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.16/5.45 fof(f197,plain,(
% 0.16/5.45 ((((((((((((![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=sK2_skl&rpoint(sK2_skl)))&(vd1186=sK3_skl&rpoint(sK3_skl)))&(vd1185=sK4_skl&rpoint(sK4_skl)))&~vd1179=vd1180)&~vd1178=vd1180)&~vd1178=vd1179)&(vd1180=sK5_skl&rpoint(sK5_skl)))&(vd1179=sK6_skl&rpoint(sK6_skl)))&(vd1178=sK7_skl&rpoint(sK7_skl))),
% 0.16/5.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl]),skolemize(Vd1191,sK2_skl),skolemize(Vd1190,sK3_skl),skolemize(Vd1189,sK4_skl),skolemize(Vd1184,sK5_skl),skolemize(Vd1183,sK6_skl),skolemize(Vd1182,sK7_skl)],[f196])).
% 0.16/5.45 fof(f202,plain,(
% 0.16/5.45 vd1187=sK2_skl),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f197])).
% 0.16/5.45 fof(f203,plain,(
% 0.16/5.45 rpoint(sK2_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f197])).
% 0.16/5.45 fof(f206,plain,(
% 0.16/5.45 vd1185=sK4_skl),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f197])).
% 0.16/5.45 fof(f207,plain,(
% 0.16/5.45 rpoint(sK4_skl)),
% 0.16/5.45 inference(cnf_transformation,[status(thm)],[f197])).
% 0.16/5.45 fof(f807,plain,(
% 0.16/5.45 ![X0,X1,X2]: (~rR(X0,X1,X2)|~rpoint(X2)|~rpoint(X0)|~rpoint(X1)|vplus(vf(X1,X0),vf(X0,X2))=vf(X1,X2))),
% 0.16/5.45 inference(destructive_equality_resolution,[status(thm)],[f169])).
% 0.16/5.45 fof(f1022,plain,(
% 0.16/5.45 ~rpoint(vd1187)|~rpoint(vd1201)|~rpoint(vd1185)|vplus(vf(vd1185,vd1201),vf(vd1201,vd1187))=vf(vd1185,vd1187)),
% 0.16/5.45 inference(resolution,[status(thm)],[f807,f163])).
% 0.16/5.45 fof(f1023,definition,(
% 0.16/5.45 sQ16_spl <=> (rpoint(vd1187))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f1025,plain,(
% 0.16/5.45 ~rpoint(vd1187)|sQ16_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f1023])).
% 0.16/5.45 fof(f1026,definition,(
% 0.16/5.45 sQ17_spl <=> (rpoint(vd1201))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f1028,plain,(
% 0.16/5.45 ~rpoint(vd1201)|sQ17_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f1026])).
% 0.16/5.45 fof(f1029,definition,(
% 0.16/5.45 sQ18_spl <=> (rpoint(vd1185))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f1031,plain,(
% 0.16/5.45 ~rpoint(vd1185)|sQ18_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f1029])).
% 0.16/5.45 fof(f1032,definition,(
% 0.16/5.45 sQ19_spl <=> (vplus(vf(vd1185,vd1201),vf(vd1201,vd1187))=vf(vd1185,vd1187))),
% 0.16/5.45 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.16/5.45 fof(f1033,plain,(
% 0.16/5.45 vplus(vf(vd1185,vd1201),vf(vd1201,vd1187))=vf(vd1185,vd1187)|~sQ19_spl),
% 0.16/5.45 inference(component_clause,[status(thm)],[f1032])).
% 0.16/5.45 fof(f1035,plain,(
% 0.16/5.45 ~sQ16_spl|~sQ17_spl|~sQ18_spl|sQ19_spl),
% 0.16/5.45 inference(split_clause,[status(thm)],[f1022,f1023,f1026,f1029,f1032])).
% 0.16/5.45 fof(f1036,plain,(
% 0.16/5.45 $false|~sQ19_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f1033,f162])).
% 0.16/5.45 fof(f1037,plain,(
% 0.16/5.45 ~sQ19_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f1036])).
% 0.16/5.45 fof(f1065,plain,(
% 0.16/5.45 rpoint(vd1201)),
% 0.16/5.45 inference(forward_demodulation,[status(thm)],[f189,f190])).
% 0.16/5.45 fof(f1089,plain,(
% 0.16/5.45 $false|sQ17_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f1028,f1065])).
% 0.16/5.45 fof(f1090,plain,(
% 0.16/5.45 sQ17_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f1089])).
% 0.16/5.45 fof(f1165,plain,(
% 0.16/5.45 rpoint(vd1187)),
% 0.16/5.45 inference(forward_demodulation,[status(thm)],[f202,f203])).
% 0.16/5.45 fof(f1166,plain,(
% 0.16/5.45 $false|sQ16_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f1165,f1025])).
% 0.16/5.45 fof(f1167,plain,(
% 0.16/5.45 sQ16_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f1166])).
% 0.16/5.45 fof(f1256,plain,(
% 0.16/5.45 rpoint(vd1185)),
% 0.16/5.45 inference(forward_demodulation,[status(thm)],[f206,f207])).
% 0.16/5.45 fof(f1257,plain,(
% 0.16/5.45 $false|sQ18_spl),
% 0.16/5.45 inference(forward_subsumption_resolution,[status(thm)],[f1256,f1031])).
% 0.16/5.45 fof(f1258,plain,(
% 0.16/5.45 sQ18_spl),
% 0.16/5.45 inference(contradiction_clause,[status(thm)],[f1257])).
% 0.16/5.45 fof(f1259,plain,(
% 0.16/5.45 $false),
% 0.16/5.45 inference(sat_refutation,[status(thm)],[f1035,f1037,f1090,f1167,f1258])).
% 0.16/5.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/5.49 % Elapsed time: 0.087368 seconds
% 0.16/5.49 % CPU time: 0.323575 seconds
% 0.16/5.49 % Total memory used: 72.731 MB
% 0.16/5.49 % Net memory used: 72.426 MB
%------------------------------------------------------------------------------