%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO305+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:21 PM UTC 2026
% Result : Theorem 0.10s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO305+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 : n003.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:25:30 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.41 % Drodi V4.1.1
% 0.10/0.44 % Refutation found
% 0.10/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.44 fof(f1,conjecture,(
% 0.10/0.44 ron(vd1302,vd1297) ),
% 0.10/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f2,negated_conjecture,(
% 0.10/0.44 ~(ron(vd1302,vd1297) )),
% 0.10/0.44 inference(negated_conjecture,[status(cth)],[f1])).
% 0.10/0.44 fof(f5,axiom,(
% 0.10/0.44 ( vd1302 = vd1303& rR(vd1289,vd1287,vd1302)& rpoint(vd1303)& rR(vd1288,vd1287,vd1299) ) ),
% 0.10/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f7,axiom,(
% 0.10/0.44 ron(vd1289,vd1297) ),
% 0.10/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f8,axiom,(
% 0.10/0.44 ron(vd1287,vd1297) ),
% 0.10/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f9,axiom,(
% 0.10/0.44 rline(vd1297) ),
% 0.10/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f13,axiom,(
% 0.10/0.44 ( vf(vd1287,vd1288) = vf(vd1287,vd1289)& vd1288 != vd1289& vd1287 != vd1289& vd1287 != vd1288& (? [Vd1293] :( vd1289 = Vd1293& rpoint(Vd1293) ))& (? [Vd1292] :( vd1288 = Vd1292& rpoint(Vd1292) ))& (? [Vd1291] :( vd1287 = Vd1291& rpoint(Vd1291) ) )) ),
% 0.10/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f14,axiom,(
% 0.10/0.44 (! [Vd352,Vd353,Vd354,Vd359,Vd360] :( ( Vd359 = Vd360& ron(Vd353,Vd359)& ron(Vd352,Vd359)& rR(Vd353,Vd352,Vd354)& rline(Vd360)& (? [Vd358] :( Vd354 = Vd358& rpoint(Vd358) ))& (? [Vd357] :( Vd353 = Vd357& rpoint(Vd357) ))& (? [Vd356] :( Vd352 = Vd356& rpoint(Vd356) ) ))=> ron(Vd354,Vd359) ) )),
% 0.10/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.44 fof(f127,plain,(
% 0.10/0.44 ~ron(vd1302,vd1297)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.44 fof(f130,plain,(
% 0.10/0.44 vd1302=vd1303),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.44 fof(f131,plain,(
% 0.10/0.44 rR(vd1289,vd1287,vd1302)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.44 fof(f132,plain,(
% 0.10/0.44 rpoint(vd1303)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.44 fof(f135,plain,(
% 0.10/0.44 ron(vd1289,vd1297)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.44 fof(f136,plain,(
% 0.10/0.44 ron(vd1287,vd1297)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.44 fof(f137,plain,(
% 0.10/0.44 rline(vd1297)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.44 fof(f141,plain,(
% 0.10/0.44 (((((vf(vd1287,vd1288)=vf(vd1287,vd1289)&~vd1288=vd1289)&~vd1287=vd1289)&~vd1287=vd1288)&(vd1289=sK0_skl&rpoint(sK0_skl)))&(vd1288=sK1_skl&rpoint(sK1_skl)))&(vd1287=sK2_skl&rpoint(sK2_skl))),
% 0.10/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(Vd1293,sK0_skl),skolemize(Vd1292,sK1_skl),skolemize(Vd1291,sK2_skl)],[f13])).
% 0.10/0.44 fof(f146,plain,(
% 0.10/0.44 vd1289=sK0_skl),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f141])).
% 0.10/0.44 fof(f147,plain,(
% 0.10/0.44 rpoint(sK0_skl)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f141])).
% 0.10/0.44 fof(f150,plain,(
% 0.10/0.44 vd1287=sK2_skl),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f141])).
% 0.10/0.44 fof(f151,plain,(
% 0.10/0.44 rpoint(sK2_skl)),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f141])).
% 0.10/0.44 fof(f152,plain,(
% 0.10/0.44 ![Vd352,Vd353,Vd354,Vd359,Vd360]: ((((((((~Vd359=Vd360|~ron(Vd353,Vd359))|~ron(Vd352,Vd359))|~rR(Vd353,Vd352,Vd354))|~rline(Vd360))|(![Vd358]: (~Vd354=Vd358|~rpoint(Vd358))))|(![Vd357]: (~Vd353=Vd357|~rpoint(Vd357))))|(![Vd356]: (~Vd352=Vd356|~rpoint(Vd356))))|ron(Vd354,Vd359))),
% 0.10/0.44 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.10/0.44 fof(f153,plain,(
% 0.10/0.44 ![Vd354,Vd359]: ((![Vd352]: ((![Vd353]: (((![Vd360]: ((((~Vd359=Vd360|~ron(Vd353,Vd359))|~ron(Vd352,Vd359))|~rR(Vd353,Vd352,Vd354))|~rline(Vd360)))|(![Vd358]: (~Vd354=Vd358|~rpoint(Vd358))))|(![Vd357]: (~Vd353=Vd357|~rpoint(Vd357)))))|(![Vd356]: (~Vd352=Vd356|~rpoint(Vd356)))))|ron(Vd354,Vd359))),
% 0.10/0.44 inference(miniscoping,[status(thm)],[f152])).
% 0.10/0.44 fof(f154,plain,(
% 0.10/0.44 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~X0=X1|~ron(X2,X0)|~ron(X3,X0)|~rR(X2,X3,X4)|~rline(X1)|~X4=X5|~rpoint(X5)|~X2=X6|~rpoint(X6)|~X3=X7|~rpoint(X7)|ron(X4,X0))),
% 0.10/0.44 inference(cnf_transformation,[status(thm)],[f153])).
% 0.10/0.44 fof(f672,plain,(
% 0.10/0.44 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X2,X1)|~rR(X0,X2,X3)|~rline(X1)|~rpoint(X3)|~rpoint(X0)|~rpoint(X2)|ron(X3,X1))),
% 0.10/0.44 inference(destructive_equality_resolution,[status(thm)],[f154])).
% 0.10/0.44 fof(f907,plain,(
% 0.10/0.44 rpoint(vd1302)),
% 0.10/0.45 inference(forward_demodulation,[status(thm)],[f130,f132])).
% 0.10/0.45 fof(f912,plain,(
% 0.10/0.45 ron(sK0_skl,vd1297)),
% 0.10/0.45 inference(backward_demodulation,[status(thm)],[f146,f135])).
% 0.10/0.45 fof(f913,plain,(
% 0.10/0.45 rR(sK0_skl,vd1287,vd1302)),
% 0.10/0.45 inference(backward_demodulation,[status(thm)],[f146,f131])).
% 0.10/0.45 fof(f917,plain,(
% 0.10/0.45 rR(sK0_skl,sK2_skl,vd1302)),
% 0.10/0.45 inference(backward_demodulation,[status(thm)],[f150,f913])).
% 0.10/0.45 fof(f919,plain,(
% 0.10/0.45 ron(sK2_skl,vd1297)),
% 0.10/0.45 inference(backward_demodulation,[status(thm)],[f150,f136])).
% 0.10/0.45 fof(f921,plain,(
% 0.10/0.45 ![X0,X1]: (~ron(X0,vd1297)|~ron(X1,vd1297)|~rR(X0,X1,vd1302)|~rline(vd1297)|~rpoint(vd1302)|~rpoint(X0)|~rpoint(X1))),
% 0.10/0.45 inference(resolution,[status(thm)],[f672,f127])).
% 0.10/0.45 fof(f922,plain,(
% 0.10/0.45 ![X0,X1]: (~ron(X0,vd1297)|~ron(X1,vd1297)|~rR(X0,X1,vd1302)|~rpoint(vd1302)|~rpoint(X0)|~rpoint(X1))),
% 0.10/0.45 inference(forward_subsumption_resolution,[status(thm)],[f921,f137])).
% 0.10/0.45 fof(f926,plain,(
% 0.10/0.45 ![X0,X1]: (~ron(X0,vd1297)|~ron(X1,vd1297)|~rR(X0,X1,vd1302)|~rpoint(X0)|~rpoint(X1))),
% 0.10/0.45 inference(forward_subsumption_resolution,[status(thm)],[f922,f907])).
% 0.10/0.45 fof(f927,plain,(
% 0.10/0.45 ~ron(sK0_skl,vd1297)|~ron(sK2_skl,vd1297)|~rpoint(sK0_skl)|~rpoint(sK2_skl)),
% 0.10/0.45 inference(resolution,[status(thm)],[f926,f917])).
% 0.10/0.45 fof(f928,plain,(
% 0.10/0.45 ~ron(sK2_skl,vd1297)|~rpoint(sK0_skl)|~rpoint(sK2_skl)),
% 0.10/0.45 inference(forward_subsumption_resolution,[status(thm)],[f927,f912])).
% 0.10/0.45 fof(f929,plain,(
% 0.10/0.45 ~rpoint(sK0_skl)|~rpoint(sK2_skl)),
% 0.10/0.45 inference(forward_subsumption_resolution,[status(thm)],[f928,f919])).
% 0.10/0.45 fof(f930,plain,(
% 0.10/0.45 ~rpoint(sK0_skl)),
% 0.10/0.45 inference(resolution,[status(thm)],[f929,f151])).
% 0.10/0.45 fof(f931,plain,(
% 0.10/0.45 $false),
% 0.10/0.45 inference(forward_subsumption_resolution,[status(thm)],[f930,f147])).
% 0.10/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.47 % Elapsed time: 0.089421 seconds
% 0.10/0.47 % CPU time: 0.255092 seconds
% 0.10/0.47 % Total memory used: 121.332 MB
% 0.10/0.47 % Net memory used: 120.984 MB
%------------------------------------------------------------------------------