%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO344+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 : n003.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:23 PM UTC 2026
% Result : Theorem 0.11s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO344+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.08/0.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 15:31:45 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.11/0.40 % Refutation found
% 0.11/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.40 fof(f1,conjecture,(
% 0.11/0.40 (! [Vdthex] :( ( ron(vd1409,Vdthex)& ron(vd1401,Vdthex)& rline(Vdthex) )=> Vdthex = vd1419 ) )),
% 0.11/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f2,negated_conjecture,(
% 0.11/0.40 ~((! [Vdthex] :( ( ron(vd1409,Vdthex)& ron(vd1401,Vdthex)& rline(Vdthex) )=> Vdthex = vd1419 ) ))),
% 0.11/0.40 inference(negated_conjecture,[status(cth)],[f1])).
% 0.11/0.40 fof(f3,axiom,(
% 0.11/0.40 ( ron(vd1409,vd1419)& ron(vd1401,vd1419)& rline(vd1419) ) ),
% 0.11/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f7,axiom,(
% 0.11/0.40 vd1409 != vd1401 ),
% 0.11/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f8,axiom,(
% 0.11/0.40 rpoint(vd1409) ),
% 0.11/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f9,axiom,(
% 0.11/0.40 ( vd1406 = vd1407& ron(vd1400,vd1406)& ron(vd1399,vd1406)& rline(vd1407)& vd1400 != vd1401& vd1399 != vd1401& vd1399 != vd1400& (? [Vd1405] :( vd1401 = Vd1405& rpoint(Vd1405) ))& (? [Vd1404] :( vd1400 = Vd1404& rpoint(Vd1404) ))& (? [Vd1403] :( vd1399 = Vd1403& rpoint(Vd1403) ) )) ),
% 0.11/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f16,axiom,(
% 0.11/0.40 (! [Vd314,Vd315,Vd319,Vd320] :( ( ron(Vd315,Vd320)& ron(Vd315,Vd319)& ron(Vd314,Vd320)& ron(Vd314,Vd319)& (? [Vd324] :( Vd320 = Vd324& rline(Vd324) ))& (? [Vd323] :( Vd319 = Vd323& rline(Vd323) ))& Vd314 != Vd315& (? [Vd318] :( Vd315 = Vd318& rpoint(Vd318) ))& (? [Vd317] :( Vd314 = Vd317& rpoint(Vd317) ) ))=> Vd319 = Vd320 ) )),
% 0.11/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.40 fof(f130,plain,(
% 0.11/0.40 (?[Vdthex]: (((ron(vd1409,Vdthex)&ron(vd1401,Vdthex))&rline(Vdthex))&~Vdthex=vd1419))),
% 0.11/0.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.11/0.40 fof(f131,plain,(
% 0.11/0.40 (((ron(vd1409,sK0_skl)&ron(vd1401,sK0_skl))&rline(sK0_skl))&~sK0_skl=vd1419)),
% 0.11/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f130])).
% 0.11/0.40 fof(f132,plain,(
% 0.11/0.40 ron(vd1409,sK0_skl)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f131])).
% 0.11/0.40 fof(f133,plain,(
% 0.11/0.40 ron(vd1401,sK0_skl)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f131])).
% 0.11/0.40 fof(f134,plain,(
% 0.11/0.40 rline(sK0_skl)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f131])).
% 0.11/0.40 fof(f135,plain,(
% 0.11/0.40 ~sK0_skl=vd1419),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f131])).
% 0.11/0.40 fof(f136,plain,(
% 0.11/0.40 ron(vd1409,vd1419)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.11/0.40 fof(f137,plain,(
% 0.11/0.40 ron(vd1401,vd1419)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.11/0.40 fof(f138,plain,(
% 0.11/0.40 rline(vd1419)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.11/0.40 fof(f145,plain,(
% 0.11/0.40 ~vd1409=vd1401),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.11/0.40 fof(f146,plain,(
% 0.11/0.40 rpoint(vd1409)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f8])).
% 0.11/0.40 fof(f147,plain,(
% 0.11/0.40 ((((((((vd1406=vd1407&ron(vd1400,vd1406))&ron(vd1399,vd1406))&rline(vd1407))&~vd1400=vd1401)&~vd1399=vd1401)&~vd1399=vd1400)&(vd1401=sK1_skl&rpoint(sK1_skl)))&(vd1400=sK2_skl&rpoint(sK2_skl)))&(vd1399=sK3_skl&rpoint(sK3_skl))),
% 0.11/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(Vd1405,sK1_skl),skolemize(Vd1404,sK2_skl),skolemize(Vd1403,sK3_skl)],[f9])).
% 0.11/0.40 fof(f155,plain,(
% 0.11/0.40 vd1401=sK1_skl),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f147])).
% 0.11/0.40 fof(f156,plain,(
% 0.11/0.40 rpoint(sK1_skl)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f147])).
% 0.11/0.40 fof(f172,plain,(
% 0.11/0.40 ![Vd314,Vd315,Vd319,Vd320]: (((((((((~ron(Vd315,Vd320)|~ron(Vd315,Vd319))|~ron(Vd314,Vd320))|~ron(Vd314,Vd319))|(![Vd324]: (~Vd320=Vd324|~rline(Vd324))))|(![Vd323]: (~Vd319=Vd323|~rline(Vd323))))|Vd314=Vd315)|(![Vd318]: (~Vd315=Vd318|~rpoint(Vd318))))|(![Vd317]: (~Vd314=Vd317|~rpoint(Vd317))))|Vd319=Vd320)),
% 0.11/0.40 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.11/0.40 fof(f173,plain,(
% 0.11/0.40 ![Vd319,Vd320]: ((![Vd314]: ((![Vd315]: (((((((~ron(Vd315,Vd320)|~ron(Vd315,Vd319))|~ron(Vd314,Vd320))|~ron(Vd314,Vd319))|(![Vd324]: (~Vd320=Vd324|~rline(Vd324))))|(![Vd323]: (~Vd319=Vd323|~rline(Vd323))))|Vd314=Vd315)|(![Vd318]: (~Vd315=Vd318|~rpoint(Vd318)))))|(![Vd317]: (~Vd314=Vd317|~rpoint(Vd317)))))|Vd319=Vd320)),
% 0.11/0.40 inference(miniscoping,[status(thm)],[f172])).
% 0.11/0.40 fof(f174,plain,(
% 0.11/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ron(X0,X1)|~ron(X0,X2)|~ron(X3,X1)|~ron(X3,X2)|~X1=X4|~rline(X4)|~X2=X5|~rline(X5)|X3=X0|~X0=X6|~rpoint(X6)|~X3=X7|~rpoint(X7)|X2=X1)),
% 0.11/0.40 inference(cnf_transformation,[status(thm)],[f173])).
% 0.11/0.40 fof(f726,plain,(
% 0.11/0.40 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~ron(X3,X1)|~ron(X3,X2)|~rline(X1)|~rline(X2)|X3=X0|~rpoint(X0)|~rpoint(X3)|X2=X1)),
% 0.11/0.40 inference(destructive_equality_resolution,[status(thm)],[f174])).
% 0.11/0.40 fof(f963,plain,(
% 0.11/0.40 ![X0,X1]: (~ron(vd1409,X0)|~ron(X1,X0)|~ron(X1,vd1419)|~rline(X0)|~rline(vd1419)|X1=vd1409|~rpoint(vd1409)|~rpoint(X1)|vd1419=X0)),
% 0.11/0.40 inference(resolution,[status(thm)],[f726,f136])).
% 0.11/0.40 fof(f981,definition,(
% 0.11/0.40 sQ9_spl <=> (rline(vd1419))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f983,plain,(
% 0.11/0.40 ~rline(vd1419)|sQ9_spl),
% 0.11/0.40 inference(component_clause,[status(thm)],[f981])).
% 0.11/0.40 fof(f987,definition,(
% 0.11/0.40 sQ11_spl <=> (rpoint(vd1401))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f989,plain,(
% 0.11/0.40 ~rpoint(vd1401)|sQ11_spl),
% 0.11/0.40 inference(component_clause,[status(thm)],[f987])).
% 0.11/0.40 fof(f998,definition,(
% 0.11/0.40 sQ14_spl <=> (ron(vd1401,sK0_skl))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f1000,plain,(
% 0.11/0.40 ~ron(vd1401,sK0_skl)|sQ14_spl),
% 0.11/0.40 inference(component_clause,[status(thm)],[f998])).
% 0.11/0.40 fof(f1001,definition,(
% 0.11/0.40 sQ15_spl <=> (rline(sK0_skl))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f1003,plain,(
% 0.11/0.40 ~rline(sK0_skl)|sQ15_spl),
% 0.11/0.40 inference(component_clause,[status(thm)],[f1001])).
% 0.11/0.40 fof(f1018,definition,(
% 0.11/0.40 sQ20_spl <=> (rpoint(vd1409))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f1020,plain,(
% 0.11/0.40 ~rpoint(vd1409)|sQ20_spl),
% 0.11/0.40 inference(component_clause,[status(thm)],[f1018])).
% 0.11/0.40 fof(f1022,definition,(
% 0.11/0.40 ![X0,X1]: (sQ21_spl <=> (~ron(vd1409,X0)|~ron(X1,X0)|~ron(X1,vd1419)|~rline(X0)|X1=vd1409|~rpoint(X1)|vd1419=X0))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f1023,plain,(
% 0.11/0.40 ![X0,X1]: (~ron(vd1409,X0)|~ron(X1,X0)|~ron(X1,vd1419)|~rline(X0)|X1=vd1409|~rpoint(X1)|vd1419=X0|~sQ21_spl)),
% 0.11/0.40 inference(component_clause,[status(thm)],[f1022])).
% 0.11/0.40 fof(f1025,plain,(
% 0.11/0.40 sQ21_spl|~sQ9_spl|~sQ20_spl),
% 0.11/0.40 inference(split_clause,[status(thm)],[f963,f1022,f981,f1018])).
% 0.11/0.40 fof(f1058,plain,(
% 0.11/0.40 $false|sQ20_spl),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1020,f146])).
% 0.11/0.40 fof(f1059,plain,(
% 0.11/0.40 sQ20_spl),
% 0.11/0.40 inference(contradiction_clause,[status(thm)],[f1058])).
% 0.11/0.40 fof(f1060,plain,(
% 0.11/0.40 $false|sQ15_spl),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1003,f134])).
% 0.11/0.40 fof(f1061,plain,(
% 0.11/0.40 sQ15_spl),
% 0.11/0.40 inference(contradiction_clause,[status(thm)],[f1060])).
% 0.11/0.40 fof(f1062,plain,(
% 0.11/0.40 $false|sQ9_spl),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f983,f138])).
% 0.11/0.40 fof(f1063,plain,(
% 0.11/0.40 sQ9_spl),
% 0.11/0.40 inference(contradiction_clause,[status(thm)],[f1062])).
% 0.11/0.40 fof(f1066,definition,(
% 0.11/0.40 ![X0]: (sQ28_spl <=> (~ron(X0,vd1419)|~ron(X0,sK0_skl)|X0=vd1409|~rpoint(X0)))),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f1067,plain,(
% 0.11/0.40 ![X0]: (~ron(X0,vd1419)|~ron(X0,sK0_skl)|X0=vd1409|~rpoint(X0)|~sQ28_spl)),
% 0.11/0.40 inference(component_clause,[status(thm)],[f1066])).
% 0.11/0.40 fof(f1069,definition,(
% 0.11/0.40 sQ29_spl <=> (sK0_skl=vd1419)),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f1070,plain,(
% 0.11/0.40 sK0_skl=vd1419|~sQ29_spl),
% 0.11/0.40 inference(component_clause,[status(thm)],[f1069])).
% 0.11/0.40 fof(f1074,plain,(
% 0.11/0.40 ~ron(vd1401,sK0_skl)|vd1401=vd1409|~rpoint(vd1401)|~sQ28_spl),
% 0.11/0.40 inference(resolution,[status(thm)],[f1067,f137])).
% 0.11/0.40 fof(f1076,definition,(
% 0.11/0.40 sQ30_spl <=> (vd1401=vd1409)),
% 0.11/0.40 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.11/0.40 fof(f1077,plain,(
% 0.11/0.40 vd1401=vd1409|~sQ30_spl),
% 0.11/0.40 inference(component_clause,[status(thm)],[f1076])).
% 0.11/0.40 fof(f1079,plain,(
% 0.11/0.40 ~sQ14_spl|sQ30_spl|~sQ11_spl|~sQ28_spl),
% 0.11/0.40 inference(split_clause,[status(thm)],[f1074,f998,f1076,f987,f1066])).
% 0.11/0.40 fof(f1082,plain,(
% 0.11/0.40 ![X0]: (~ron(X0,sK0_skl)|~ron(X0,vd1419)|~rline(sK0_skl)|X0=vd1409|~rpoint(X0)|vd1419=sK0_skl|~sQ21_spl)),
% 0.11/0.40 inference(resolution,[status(thm)],[f1023,f132])).
% 0.11/0.40 fof(f1084,plain,(
% 0.11/0.40 sQ28_spl|~sQ15_spl|sQ29_spl|~sQ21_spl),
% 0.11/0.40 inference(split_clause,[status(thm)],[f1082,f1066,f1001,f1069,f1022])).
% 0.11/0.40 fof(f1085,plain,(
% 0.11/0.40 $false|~sQ29_spl),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1070,f135])).
% 0.11/0.40 fof(f1086,plain,(
% 0.11/0.40 ~sQ29_spl),
% 0.11/0.40 inference(contradiction_clause,[status(thm)],[f1085])).
% 0.11/0.40 fof(f1098,plain,(
% 0.11/0.40 ~rpoint(sK1_skl)|sQ11_spl),
% 0.11/0.40 inference(backward_demodulation,[status(thm)],[f155,f989])).
% 0.11/0.40 fof(f1102,plain,(
% 0.11/0.40 ~vd1409=sK1_skl),
% 0.11/0.40 inference(backward_demodulation,[status(thm)],[f155,f145])).
% 0.11/0.40 fof(f1103,plain,(
% 0.11/0.40 ron(sK1_skl,sK0_skl)),
% 0.11/0.40 inference(backward_demodulation,[status(thm)],[f155,f133])).
% 0.11/0.40 fof(f1124,plain,(
% 0.11/0.40 ~ron(sK1_skl,sK0_skl)|sQ14_spl),
% 0.11/0.40 inference(forward_demodulation,[status(thm)],[f155,f1000])).
% 0.11/0.40 fof(f1139,plain,(
% 0.11/0.40 $false|sQ14_spl),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1124,f1103])).
% 0.11/0.40 fof(f1140,plain,(
% 0.11/0.40 sQ14_spl),
% 0.11/0.40 inference(contradiction_clause,[status(thm)],[f1139])).
% 0.11/0.40 fof(f1142,plain,(
% 0.11/0.40 $false|sQ11_spl),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1098,f156])).
% 0.11/0.40 fof(f1143,plain,(
% 0.11/0.40 sQ11_spl),
% 0.11/0.40 inference(contradiction_clause,[status(thm)],[f1142])).
% 0.11/0.40 fof(f1144,plain,(
% 0.11/0.40 sK1_skl=vd1409|~sQ30_spl),
% 0.11/0.40 inference(forward_demodulation,[status(thm)],[f155,f1077])).
% 0.11/0.40 fof(f1150,plain,(
% 0.11/0.40 $false|~sQ30_spl),
% 0.11/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1144,f1102])).
% 0.11/0.40 fof(f1151,plain,(
% 0.11/0.40 ~sQ30_spl),
% 0.11/0.40 inference(contradiction_clause,[status(thm)],[f1150])).
% 0.11/0.40 fof(f1152,plain,(
% 0.11/0.40 $false),
% 0.11/0.40 inference(sat_refutation,[status(thm)],[f1025,f1059,f1061,f1063,f1079,f1084,f1086,f1140,f1143,f1151])).
% 0.11/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.11/0.43 % Elapsed time: 0.076353 seconds
% 0.11/0.43 % CPU time: 0.233673 seconds
% 0.11/0.43 % Total memory used: 87.984 MB
% 0.11/0.43 % Net memory used: 87.680 MB
%------------------------------------------------------------------------------