%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO291+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 : n006.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 10.96s 2.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO291+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n006.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 20 15:15:27 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.51 % Drodi V4.1.1
% 10.96/2.04 % Refutation found
% 10.96/2.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.96/2.04 % SZS output start CNFRefutation for theBenchmark
% 10.96/2.04 fof(f1,conjecture,(
% 10.96/2.04 ( rS(vd1200,vd1187,vd1234)| rS(vd1186,vd1201,vd1232) ) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f2,negated_conjecture,(
% 10.96/2.04 ~(( rS(vd1200,vd1187,vd1234)| rS(vd1186,vd1201,vd1232) ) )),
% 10.96/2.04 inference(negated_conjecture,[status(cth)],[f1])).
% 10.96/2.04 fof(f4,axiom,(
% 10.96/2.04 ~ ron(vd1201,vd1232) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f5,axiom,(
% 10.96/2.04 ron(vd1185,vd1232) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f6,axiom,(
% 10.96/2.04 rline(vd1232) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f9,axiom,(
% 10.96/2.04 (? [Vd1205] :( vd1201 = Vd1205& rpoint(Vd1205) ) )),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f11,axiom,(
% 10.96/2.04 rline(vd1197) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f12,axiom,(
% 10.96/2.04 ( ~ (? [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) ) )) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f16,axiom,(
% 10.96/2.04 ron(vd1187,vd1232) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f17,axiom,(
% 10.96/2.04 ron(vd1200,vd1197) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f19,axiom,(
% 10.96/2.04 ron(vd1185,vd1197) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f21,axiom,(
% 10.96/2.04 vd1199 = vd1185 ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f25,axiom,(
% 10.96/2.04 vd1200 = vd1186 ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f33,axiom,(
% 10.96/2.04 (? [Vd1203] :( vd1199 = Vd1203& rpoint(Vd1203) ) )),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f45,axiom,(
% 10.96/2.04 rS(vd1187,vd1201,vd1197) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f46,axiom,(
% 10.96/2.04 ron(vd1201,vd1234) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f47,axiom,(
% 10.96/2.04 ron(vd1185,vd1234) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f48,axiom,(
% 10.96/2.04 rline(vd1234) ),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f90,axiom,(
% 10.96/2.04 (! [Vd537,Vd538,Vd539,Vd544,Vd545,Vd546,Vd547] :( ( Vd545 != Vd544& ~ ron(Vd547,Vd538)& ~ rS(Vd545,Vd547,Vd538)& rS(Vd546,Vd547,Vd537)& ron(Vd547,Vd539)& ron(Vd546,Vd538)& ron(Vd545,Vd537)& ron(Vd544,Vd539)& ron(Vd544,Vd538)& ron(Vd544,Vd537)& (? [Vd552] :( Vd547 = Vd552& rpoint(Vd552) ))& (? [Vd551] :( Vd546 = Vd551& rpoint(Vd551) ))& (? [Vd550] :( Vd545 = Vd550& rpoint(Vd550) ))& (? [Vd549] :( Vd544 = Vd549& rpoint(Vd549) ))& (? [Vd543] :( Vd539 = Vd543& rline(Vd543) ))& (? [Vd542] :( Vd538 = Vd542& rline(Vd542) ))& (? [Vd541] :( Vd537 = Vd541& rline(Vd541) ) ))=> rS(Vd545,Vd546,Vd539) ) )),
% 10.96/2.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.96/2.04 fof(f152,plain,(
% 10.96/2.04 (~rS(vd1200,vd1187,vd1234)&~rS(vd1186,vd1201,vd1232))),
% 10.96/2.04 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 10.96/2.04 fof(f153,plain,(
% 10.96/2.04 ~rS(vd1200,vd1187,vd1234)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f152])).
% 10.96/2.04 fof(f154,plain,(
% 10.96/2.04 ~rS(vd1186,vd1201,vd1232)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f152])).
% 10.96/2.04 fof(f156,plain,(
% 10.96/2.04 ~ron(vd1201,vd1232)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f4])).
% 10.96/2.04 fof(f157,plain,(
% 10.96/2.04 ron(vd1185,vd1232)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f5])).
% 10.96/2.04 fof(f158,plain,(
% 10.96/2.04 rline(vd1232)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f6])).
% 10.96/2.04 fof(f161,plain,(
% 10.96/2.04 (vd1201=sK0_skl&rpoint(sK0_skl))),
% 10.96/2.04 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1205,sK0_skl)],[f9])).
% 10.96/2.04 fof(f162,plain,(
% 10.96/2.04 vd1201=sK0_skl),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f161])).
% 10.96/2.04 fof(f163,plain,(
% 10.96/2.04 rpoint(sK0_skl)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f161])).
% 10.96/2.04 fof(f165,plain,(
% 10.96/2.04 rline(vd1197)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f11])).
% 10.96/2.04 fof(f166,plain,(
% 10.96/2.04 ((((((((((((![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)))),
% 10.96/2.04 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 10.96/2.04 fof(f167,plain,(
% 10.96/2.04 ((((((((((((![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))),
% 10.96/2.04 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)],[f166])).
% 10.96/2.04 fof(f168,plain,(
% 10.96/2.04 ![X0]: (~ron(vd1187,X0)|~ron(vd1186,X0)|~ron(vd1185,X0)|~rline(X0))),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f167])).
% 10.96/2.04 fof(f172,plain,(
% 10.96/2.04 vd1187=sK1_skl),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f167])).
% 10.96/2.04 fof(f173,plain,(
% 10.96/2.04 rpoint(sK1_skl)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f167])).
% 10.96/2.04 fof(f174,plain,(
% 10.96/2.04 vd1186=sK2_skl),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f167])).
% 10.96/2.04 fof(f175,plain,(
% 10.96/2.04 rpoint(sK2_skl)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f167])).
% 10.96/2.04 fof(f197,plain,(
% 10.96/2.04 ron(vd1187,vd1232)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f16])).
% 10.96/2.04 fof(f198,plain,(
% 10.96/2.04 ron(vd1200,vd1197)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f17])).
% 10.96/2.04 fof(f200,plain,(
% 10.96/2.04 ron(vd1185,vd1197)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f19])).
% 10.96/2.04 fof(f202,plain,(
% 10.96/2.04 vd1199=vd1185),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f21])).
% 10.96/2.04 fof(f206,plain,(
% 10.96/2.04 vd1200=vd1186),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f25])).
% 10.96/2.04 fof(f216,plain,(
% 10.96/2.04 (vd1199=sK8_skl&rpoint(sK8_skl))),
% 10.96/2.04 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Vd1203,sK8_skl)],[f33])).
% 10.96/2.04 fof(f217,plain,(
% 10.96/2.04 vd1199=sK8_skl),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f216])).
% 10.96/2.04 fof(f218,plain,(
% 10.96/2.04 rpoint(sK8_skl)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f216])).
% 10.96/2.04 fof(f244,plain,(
% 10.96/2.04 rS(vd1187,vd1201,vd1197)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f45])).
% 10.96/2.04 fof(f245,plain,(
% 10.96/2.04 ron(vd1201,vd1234)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f46])).
% 10.96/2.04 fof(f246,plain,(
% 10.96/2.04 ron(vd1185,vd1234)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f47])).
% 10.96/2.04 fof(f247,plain,(
% 10.96/2.04 rline(vd1234)),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f48])).
% 10.96/2.04 fof(f394,plain,(
% 10.96/2.04 ![Vd537,Vd538,Vd539,Vd544,Vd545,Vd546,Vd547]: (((((((((((((((((Vd545=Vd544|ron(Vd547,Vd538))|rS(Vd545,Vd547,Vd538))|~rS(Vd546,Vd547,Vd537))|~ron(Vd547,Vd539))|~ron(Vd546,Vd538))|~ron(Vd545,Vd537))|~ron(Vd544,Vd539))|~ron(Vd544,Vd538))|~ron(Vd544,Vd537))|(![Vd552]: (~Vd547=Vd552|~rpoint(Vd552))))|(![Vd551]: (~Vd546=Vd551|~rpoint(Vd551))))|(![Vd550]: (~Vd545=Vd550|~rpoint(Vd550))))|(![Vd549]: (~Vd544=Vd549|~rpoint(Vd549))))|(![Vd543]: (~Vd539=Vd543|~rline(Vd543))))|(![Vd542]: (~Vd538=Vd542|~rline(Vd542))))|(![Vd541]: (~Vd537=Vd541|~rline(Vd541))))|rS(Vd545,Vd546,Vd539))),
% 10.96/2.04 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 10.96/2.04 fof(f395,plain,(
% 10.96/2.04 ![Vd539,Vd545,Vd546]: ((![Vd537]: ((![Vd538]: (((![Vd544]: ((((![Vd547]: ((((((((((Vd545=Vd544|ron(Vd547,Vd538))|rS(Vd545,Vd547,Vd538))|~rS(Vd546,Vd547,Vd537))|~ron(Vd547,Vd539))|~ron(Vd546,Vd538))|~ron(Vd545,Vd537))|~ron(Vd544,Vd539))|~ron(Vd544,Vd538))|~ron(Vd544,Vd537))|(![Vd552]: (~Vd547=Vd552|~rpoint(Vd552)))))|(![Vd551]: (~Vd546=Vd551|~rpoint(Vd551))))|(![Vd550]: (~Vd545=Vd550|~rpoint(Vd550))))|(![Vd549]: (~Vd544=Vd549|~rpoint(Vd549)))))|(![Vd543]: (~Vd539=Vd543|~rline(Vd543))))|(![Vd542]: (~Vd538=Vd542|~rline(Vd542)))))|(![Vd541]: (~Vd537=Vd541|~rline(Vd541)))))|rS(Vd545,Vd546,Vd539))),
% 10.96/2.04 inference(miniscoping,[status(thm)],[f394])).
% 10.96/2.04 fof(f396,plain,(
% 10.96/2.04 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (X0=X1|ron(X2,X3)|rS(X0,X2,X3)|~rS(X4,X2,X5)|~ron(X2,X6)|~ron(X4,X3)|~ron(X0,X5)|~ron(X1,X6)|~ron(X1,X3)|~ron(X1,X5)|~X2=X7|~rpoint(X7)|~X4=X8|~rpoint(X8)|~X0=X9|~rpoint(X9)|~X1=X10|~rpoint(X10)|~X6=X11|~rline(X11)|~X3=X12|~rline(X12)|~X5=X13|~rline(X13)|rS(X0,X4,X6))),
% 10.96/2.04 inference(cnf_transformation,[status(thm)],[f395])).
% 10.96/2.04 fof(f803,plain,(
% 10.96/2.04 ![X0,X1,X2,X3,X4,X5,X6]: (X0=X1|ron(X2,X3)|rS(X0,X2,X3)|~rS(X4,X2,X5)|~ron(X2,X6)|~ron(X4,X3)|~ron(X0,X5)|~ron(X1,X6)|~ron(X1,X3)|~ron(X1,X5)|~rpoint(X2)|~rpoint(X4)|~rpoint(X0)|~rpoint(X1)|~rline(X6)|~rline(X3)|~rline(X5)|rS(X0,X4,X6))),
% 10.96/2.04 inference(destructive_equality_resolution,[status(thm)],[f396])).
% 10.96/2.04 fof(f948,plain,(
% 10.96/2.04 ~rS(vd1186,vd1187,vd1234)),
% 10.96/2.04 inference(backward_demodulation,[status(thm)],[f206,f153])).
% 10.96/2.04 fof(f950,plain,(
% 10.96/2.04 ~ron(vd1186,vd1232)|~ron(vd1185,vd1232)|~rline(vd1232)),
% 10.96/2.04 inference(resolution,[status(thm)],[f168,f197])).
% 10.96/2.04 fof(f951,plain,(
% 10.96/2.04 ~ron(vd1186,vd1232)|~rline(vd1232)),
% 10.96/2.04 inference(forward_subsumption_resolution,[status(thm)],[f950,f157])).
% 10.96/2.04 fof(f952,plain,(
% 10.96/2.04 rpoint(vd1201)),
% 10.96/2.04 inference(forward_demodulation,[status(thm)],[f162,f163])).
% 10.96/2.04 fof(f953,plain,(
% 10.96/2.04 rpoint(vd1187)),
% 10.96/2.04 inference(forward_demodulation,[status(thm)],[f172,f173])).
% 10.96/2.04 fof(f954,plain,(
% 10.96/2.04 rpoint(vd1186)),
% 10.96/2.04 inference(forward_demodulation,[status(thm)],[f174,f175])).
% 10.96/2.04 fof(f956,plain,(
% 10.96/2.04 ~ron(vd1186,vd1232)),
% 10.96/2.04 inference(forward_subsumption_resolution,[status(thm)],[f951,f158])).
% 10.96/2.04 fof(f999,plain,(
% 10.96/2.04 ron(vd1199,vd1234)),
% 10.96/2.04 inference(backward_demodulation,[status(thm)],[f202,f246])).
% 10.96/2.04 fof(f1000,plain,(
% 10.96/2.04 ron(vd1199,vd1232)),
% 10.96/2.04 inference(backward_demodulation,[status(thm)],[f202,f157])).
% 10.96/2.04 fof(f1003,plain,(
% 10.96/2.04 rpoint(vd1199)),
% 10.96/2.04 inference(forward_demodulation,[status(thm)],[f217,f218])).
% 10.96/2.04 fof(f1179,plain,(
% 10.96/2.04 ron(vd1186,vd1197)),
% 10.96/2.04 inference(forward_demodulation,[status(thm)],[f206,f198])).
% 10.96/2.04 fof(f1186,plain,(
% 10.96/2.04 ron(vd1199,vd1197)),
% 10.96/2.04 inference(forward_demodulation,[status(thm)],[f202,f200])).
% 10.96/2.04 fof(f1380,plain,(
% 10.96/2.04 ![X0,X1,X2,X3]: (vd1186=X0|ron(X1,X2)|rS(vd1186,X1,X2)|~rS(vd1187,X1,X3)|~ron(X1,vd1234)|~ron(vd1187,X2)|~ron(vd1186,X3)|~ron(X0,vd1234)|~ron(X0,X2)|~ron(X0,X3)|~rpoint(X1)|~rpoint(vd1187)|~rpoint(vd1186)|~rpoint(X0)|~rline(vd1234)|~rline(X2)|~rline(X3))),
% 10.96/2.04 inference(resolution,[status(thm)],[f803,f948])).
% 10.96/2.04 fof(f1423,plain,(
% 10.96/2.04 ![X0,X1,X2,X3]: (vd1186=X0|ron(X1,X2)|rS(vd1186,X1,X2)|~rS(vd1187,X1,X3)|~ron(X1,vd1234)|~ron(vd1187,X2)|~ron(vd1186,X3)|~ron(X0,vd1234)|~ron(X0,X2)|~ron(X0,X3)|~rpoint(X1)|~rpoint(vd1186)|~rpoint(X0)|~rline(vd1234)|~rline(X2)|~rline(X3))),
% 10.96/2.04 inference(forward_subsumption_resolution,[status(thm)],[f1380,f953])).
% 10.96/2.04 fof(f1609,plain,(
% 10.96/2.04 ![X0,X1,X2,X3]: (vd1186=X0|ron(X1,X2)|rS(vd1186,X1,X2)|~rS(vd1187,X1,X3)|~ron(X1,vd1234)|~ron(vd1187,X2)|~ron(vd1186,X3)|~ron(X0,vd1234)|~ron(X0,X2)|~ron(X0,X3)|~rpoint(X1)|~rpoint(X0)|~rline(vd1234)|~rline(X2)|~rline(X3))),
% 10.96/2.04 inference(forward_subsumption_resolution,[status(thm)],[f1423,f954])).
% 10.96/2.04 fof(f1612,plain,(
% 10.96/2.04 ![X0,X1]: (vd1186=X0|ron(vd1201,X1)|rS(vd1186,vd1201,X1)|~ron(vd1201,vd1234)|~ron(vd1187,X1)|~ron(vd1186,vd1197)|~ron(X0,vd1234)|~ron(X0,X1)|~ron(X0,vd1197)|~rpoint(vd1201)|~rpoint(X0)|~rline(vd1234)|~rline(X1)|~rline(vd1197))),
% 10.96/2.04 inference(resolution,[status(thm)],[f1609,f244])).
% 10.96/2.04 fof(f1615,plain,(
% 10.96/2.04 ![X0,X1]: (vd1186=X0|ron(vd1201,X1)|rS(vd1186,vd1201,X1)|~ron(vd1187,X1)|~ron(vd1186,vd1197)|~ron(X0,vd1234)|~ron(X0,X1)|~ron(X0,vd1197)|~rpoint(vd1201)|~rpoint(X0)|~rline(vd1234)|~rline(X1)|~rline(vd1197))),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1612,f245])).
% 10.95/2.06 fof(f1620,plain,(
% 10.95/2.06 ![X0,X1]: (vd1186=X0|ron(vd1201,X1)|rS(vd1186,vd1201,X1)|~ron(vd1187,X1)|~ron(X0,vd1234)|~ron(X0,X1)|~ron(X0,vd1197)|~rpoint(vd1201)|~rpoint(X0)|~rline(vd1234)|~rline(X1)|~rline(vd1197))),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1615,f1179])).
% 10.95/2.06 fof(f1621,plain,(
% 10.95/2.06 ![X0]: (vd1186=X0|ron(vd1201,vd1232)|rS(vd1186,vd1201,vd1232)|~ron(X0,vd1234)|~ron(X0,vd1232)|~ron(X0,vd1197)|~rpoint(vd1201)|~rpoint(X0)|~rline(vd1234)|~rline(vd1232)|~rline(vd1197))),
% 10.95/2.06 inference(resolution,[status(thm)],[f1620,f197])).
% 10.95/2.06 fof(f1622,plain,(
% 10.95/2.06 ![X0]: (vd1186=X0|rS(vd1186,vd1201,vd1232)|~ron(X0,vd1234)|~ron(X0,vd1232)|~ron(X0,vd1197)|~rpoint(vd1201)|~rpoint(X0)|~rline(vd1234)|~rline(vd1232)|~rline(vd1197))),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1621,f156])).
% 10.95/2.06 fof(f1623,plain,(
% 10.95/2.06 ![X0]: (vd1186=X0|~ron(X0,vd1234)|~ron(X0,vd1232)|~ron(X0,vd1197)|~rpoint(vd1201)|~rpoint(X0)|~rline(vd1234)|~rline(vd1232)|~rline(vd1197))),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1622,f154])).
% 10.95/2.06 fof(f1624,plain,(
% 10.95/2.06 vd1186=vd1199|~ron(vd1199,vd1232)|~ron(vd1199,vd1197)|~rpoint(vd1201)|~rpoint(vd1199)|~rline(vd1234)|~rline(vd1232)|~rline(vd1197)),
% 10.95/2.06 inference(resolution,[status(thm)],[f1623,f999])).
% 10.95/2.06 fof(f1626,plain,(
% 10.95/2.06 vd1186=vd1199|~ron(vd1199,vd1197)|~rpoint(vd1201)|~rpoint(vd1199)|~rline(vd1234)|~rline(vd1232)|~rline(vd1197)),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1624,f1000])).
% 10.95/2.06 fof(f1628,plain,(
% 10.95/2.06 vd1186=vd1199|~rpoint(vd1201)|~rpoint(vd1199)|~rline(vd1234)|~rline(vd1232)|~rline(vd1197)),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1626,f1186])).
% 10.95/2.06 fof(f1629,plain,(
% 10.95/2.06 vd1186=vd1199|~rpoint(vd1199)|~rline(vd1234)|~rline(vd1232)|~rline(vd1197)),
% 10.95/2.06 inference(resolution,[status(thm)],[f1628,f952])).
% 10.95/2.06 fof(f1634,plain,(
% 10.95/2.06 vd1186=vd1199|~rline(vd1234)|~rline(vd1232)|~rline(vd1197)),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1629,f1003])).
% 10.95/2.06 fof(f1750,plain,(
% 10.95/2.06 vd1186=vd1199|~rline(vd1232)|~rline(vd1197)),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1634,f247])).
% 10.95/2.06 fof(f1751,plain,(
% 10.95/2.06 vd1186=vd1199|~rline(vd1197)),
% 10.95/2.06 inference(resolution,[status(thm)],[f1750,f158])).
% 10.95/2.06 fof(f1753,plain,(
% 10.95/2.06 vd1186=vd1199),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1751,f165])).
% 10.95/2.06 fof(f1775,plain,(
% 10.95/2.06 ~ron(vd1199,vd1232)),
% 10.95/2.06 inference(backward_demodulation,[status(thm)],[f1753,f956])).
% 10.95/2.06 fof(f1817,plain,(
% 10.95/2.06 $false),
% 10.95/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1775,f1000])).
% 10.95/2.06 % SZS output end CNFRefutation for theBenchmark.p
% 10.95/2.09 % Elapsed time: 1.603218 seconds
% 10.95/2.09 % CPU time: 11.993582 seconds
% 10.95/2.09 % Total memory used: 161.073 MB
% 10.95/2.09 % Net memory used: 156.033 MB
%------------------------------------------------------------------------------