%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO343+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 : n004.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.12s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO343+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n004.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 20 15:34:34 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.12/0.43 % Refutation found
% 0.12/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.43 fof(f1,conjecture,(
% 0.12/0.43 (! [Vdthex] :( ( ron(vd1399,Vdthex)& ron(vd1401,Vdthex)& rline(Vdthex) )=> Vdthex = vd1416 ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f2,negated_conjecture,(
% 0.12/0.43 ~((! [Vdthex] :( ( ron(vd1399,Vdthex)& ron(vd1401,Vdthex)& rline(Vdthex) )=> Vdthex = vd1416 ) ))),
% 0.12/0.43 inference(negated_conjecture,[status(cth)],[f1])).
% 0.12/0.43 fof(f3,axiom,(
% 0.12/0.43 ( ron(vd1399,vd1416)& ron(vd1401,vd1416)& rline(vd1416) ) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f5,axiom,(
% 0.12/0.43 ( 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.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f50,axiom,(
% 0.12/0.43 (! [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.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f127,plain,(
% 0.12/0.43 (?[Vdthex]: (((ron(vd1399,Vdthex)&ron(vd1401,Vdthex))&rline(Vdthex))&~Vdthex=vd1416))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.43 fof(f128,plain,(
% 0.12/0.43 (((ron(vd1399,sK0_skl)&ron(vd1401,sK0_skl))&rline(sK0_skl))&~sK0_skl=vd1416)),
% 0.12/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f127])).
% 0.12/0.43 fof(f129,plain,(
% 0.12/0.43 ron(vd1399,sK0_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f128])).
% 0.12/0.43 fof(f130,plain,(
% 0.12/0.43 ron(vd1401,sK0_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f128])).
% 0.12/0.43 fof(f131,plain,(
% 0.12/0.43 rline(sK0_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f128])).
% 0.12/0.43 fof(f132,plain,(
% 0.12/0.43 ~sK0_skl=vd1416),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f128])).
% 0.12/0.43 fof(f133,plain,(
% 0.12/0.43 ron(vd1399,vd1416)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.43 fof(f134,plain,(
% 0.12/0.43 ron(vd1401,vd1416)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.43 fof(f135,plain,(
% 0.12/0.43 rline(vd1416)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.43 fof(f137,plain,(
% 0.12/0.43 ((((((((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.12/0.43 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)],[f5])).
% 0.12/0.43 fof(f143,plain,(
% 0.12/0.43 ~vd1399=vd1401),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f137])).
% 0.12/0.43 fof(f145,plain,(
% 0.12/0.43 vd1401=sK1_skl),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f137])).
% 0.12/0.43 fof(f146,plain,(
% 0.12/0.43 rpoint(sK1_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f137])).
% 0.12/0.43 fof(f149,plain,(
% 0.12/0.43 vd1399=sK3_skl),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f137])).
% 0.12/0.43 fof(f150,plain,(
% 0.12/0.43 rpoint(sK3_skl)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f137])).
% 0.12/0.43 fof(f300,plain,(
% 0.12/0.43 ![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.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.12/0.43 fof(f301,plain,(
% 0.12/0.43 ![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.12/0.43 inference(miniscoping,[status(thm)],[f300])).
% 0.12/0.43 fof(f302,plain,(
% 0.12/0.43 ![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.12/0.43 inference(cnf_transformation,[status(thm)],[f301])).
% 0.12/0.43 fof(f785,plain,(
% 0.12/0.43 ![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.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f302])).
% 0.12/0.43 fof(f972,definition,(
% 0.12/0.43 sQ9_spl <=> (rline(vd1416))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f974,plain,(
% 0.12/0.43 ~rline(vd1416)|sQ9_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f972])).
% 0.12/0.43 fof(f992,definition,(
% 0.12/0.43 sQ15_spl <=> (rline(sK0_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f994,plain,(
% 0.12/0.43 ~rline(sK0_skl)|sQ15_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f992])).
% 0.12/0.43 fof(f1049,plain,(
% 0.12/0.43 $false|sQ15_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f994,f131])).
% 0.12/0.43 fof(f1050,plain,(
% 0.12/0.43 sQ15_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f1049])).
% 0.12/0.43 fof(f1099,plain,(
% 0.12/0.43 ron(sK1_skl,vd1416)),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f145,f134])).
% 0.12/0.43 fof(f1100,plain,(
% 0.12/0.43 ~vd1399=sK1_skl),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f145,f143])).
% 0.12/0.43 fof(f1101,plain,(
% 0.12/0.43 ron(sK1_skl,sK0_skl)),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f145,f130])).
% 0.12/0.43 fof(f1105,plain,(
% 0.12/0.43 ron(sK3_skl,vd1416)),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f149,f133])).
% 0.12/0.43 fof(f1106,plain,(
% 0.12/0.43 ron(sK3_skl,sK0_skl)),
% 0.12/0.43 inference(backward_demodulation,[status(thm)],[f149,f129])).
% 0.12/0.43 fof(f1141,plain,(
% 0.12/0.43 $false|sQ9_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f974,f135])).
% 0.12/0.43 fof(f1142,plain,(
% 0.12/0.43 sQ9_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f1141])).
% 0.12/0.43 fof(f1161,definition,(
% 0.12/0.43 sQ36_spl <=> (rpoint(sK3_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1163,plain,(
% 0.12/0.43 ~rpoint(sK3_skl)|sQ36_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1161])).
% 0.12/0.43 fof(f1173,plain,(
% 0.12/0.43 $false|sQ36_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1163,f150])).
% 0.12/0.43 fof(f1174,plain,(
% 0.12/0.43 sQ36_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f1173])).
% 0.12/0.43 fof(f1181,plain,(
% 0.12/0.43 ![X0,X1]: (~ron(X0,X1)|~ron(X0,sK0_skl)|~ron(sK1_skl,X1)|~rline(X1)|~rline(sK0_skl)|sK1_skl=X0|~rpoint(X0)|~rpoint(sK1_skl)|sK0_skl=X1)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1101,f785])).
% 0.12/0.43 fof(f1192,definition,(
% 0.12/0.43 sQ40_spl <=> (rpoint(sK1_skl))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1194,plain,(
% 0.12/0.43 ~rpoint(sK1_skl)|sQ40_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1192])).
% 0.12/0.43 fof(f1196,definition,(
% 0.12/0.43 ![X0,X1]: (sQ41_spl <=> (~ron(X0,X1)|~ron(X0,sK0_skl)|~ron(sK1_skl,X1)|~rline(X1)|sK1_skl=X0|~rpoint(X0)|sK0_skl=X1))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1197,plain,(
% 0.12/0.43 ![X0,X1]: (~ron(X0,X1)|~ron(X0,sK0_skl)|~ron(sK1_skl,X1)|~rline(X1)|sK1_skl=X0|~rpoint(X0)|sK0_skl=X1|~sQ41_spl)),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1196])).
% 0.12/0.43 fof(f1199,plain,(
% 0.12/0.43 sQ41_spl|~sQ15_spl|~sQ40_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1181,f1196,f992,f1192])).
% 0.12/0.43 fof(f1204,plain,(
% 0.12/0.43 $false|sQ40_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1194,f146])).
% 0.12/0.43 fof(f1205,plain,(
% 0.12/0.43 sQ40_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f1204])).
% 0.12/0.43 fof(f1226,plain,(
% 0.12/0.43 ![X0]: (~ron(sK3_skl,X0)|~ron(sK1_skl,X0)|~rline(X0)|sK1_skl=sK3_skl|~rpoint(sK3_skl)|sK0_skl=X0|~sQ41_spl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1197,f1106])).
% 0.12/0.43 fof(f1233,definition,(
% 0.12/0.43 ![X0]: (sQ45_spl <=> (~ron(sK3_skl,X0)|~ron(sK1_skl,X0)|~rline(X0)|sK0_skl=X0))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1234,plain,(
% 0.12/0.43 ![X0]: (~ron(sK3_skl,X0)|~ron(sK1_skl,X0)|~rline(X0)|sK0_skl=X0|~sQ45_spl)),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1233])).
% 0.12/0.43 fof(f1236,definition,(
% 0.12/0.43 sQ46_spl <=> (sK1_skl=sK3_skl)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1237,plain,(
% 0.12/0.43 sK1_skl=sK3_skl|~sQ46_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1236])).
% 0.12/0.43 fof(f1239,plain,(
% 0.12/0.43 sQ45_spl|sQ46_spl|~sQ36_spl|~sQ41_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1226,f1233,f1236,f1161,f1196])).
% 0.12/0.43 fof(f1259,plain,(
% 0.12/0.43 ~sK3_skl=sK1_skl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f149,f1100])).
% 0.12/0.43 fof(f1292,definition,(
% 0.12/0.43 sQ50_spl <=> (ron(sK3_skl,vd1416))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1294,plain,(
% 0.12/0.43 ~ron(sK3_skl,vd1416)|sQ50_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1292])).
% 0.12/0.43 fof(f1447,plain,(
% 0.12/0.43 ~ron(sK3_skl,vd1416)|~rline(vd1416)|sK0_skl=vd1416|~sQ45_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f1234,f1099])).
% 0.12/0.43 fof(f1449,definition,(
% 0.12/0.43 sQ71_spl <=> (sK0_skl=vd1416)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f1450,plain,(
% 0.12/0.43 sK0_skl=vd1416|~sQ71_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f1449])).
% 0.12/0.43 fof(f1452,plain,(
% 0.12/0.43 ~sQ50_spl|~sQ9_spl|sQ71_spl|~sQ45_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f1447,f1292,f972,f1449,f1233])).
% 0.12/0.43 fof(f1453,plain,(
% 0.12/0.43 $false|sQ50_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1294,f1105])).
% 0.12/0.43 fof(f1454,plain,(
% 0.12/0.43 sQ50_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f1453])).
% 0.12/0.43 fof(f1455,plain,(
% 0.12/0.43 $false|~sQ71_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1450,f132])).
% 0.12/0.43 fof(f1456,plain,(
% 0.12/0.43 ~sQ71_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f1455])).
% 0.12/0.43 fof(f1457,plain,(
% 0.12/0.43 $false|~sQ46_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1237,f1259])).
% 0.12/0.43 fof(f1458,plain,(
% 0.12/0.43 ~sQ46_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f1457])).
% 0.12/0.43 fof(f1459,plain,(
% 0.12/0.43 $false),
% 0.12/0.43 inference(sat_refutation,[status(thm)],[f1050,f1142,f1174,f1199,f1205,f1239,f1452,f1454,f1456,f1458])).
% 0.12/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.46 % Elapsed time: 0.085747 seconds
% 0.12/0.46 % CPU time: 0.300007 seconds
% 0.12/0.46 % Total memory used: 122.544 MB
% 0.12/0.46 % Net memory used: 122.046 MB
%------------------------------------------------------------------------------