%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO298+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 : n009.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.84s 0.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO298+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 15:13:13 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.84/0.63 % Refutation found
% 0.84/0.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.84/0.63 % SZS output start CNFRefutation for theBenchmark
% 0.84/0.63 fof(f1,conjecture,(
% 0.84/0.63 ( rR(vd1201,vd1185,vd1187)| rR(vd1187,vd1185,vd1201) ) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f2,negated_conjecture,(
% 0.84/0.63 ~(( rR(vd1201,vd1185,vd1187)| rR(vd1187,vd1185,vd1201) ) )),
% 0.84/0.63 inference(negated_conjecture,[status(cth)],[f1])).
% 0.84/0.63 fof(f3,axiom,(
% 0.84/0.63 vd1201 != vd1187 ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f4,axiom,(
% 0.84/0.63 ~ rR(vd1185,vd1201,vd1187) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f6,axiom,(
% 0.84/0.63 (! [Vd396,Vd397,Vd398,Vd403,Vd404] :( ( Vd403 = Vd404& ron(Vd398,Vd403)& ron(Vd397,Vd403)& ron(Vd396,Vd403)& rline(Vd404)& Vd397 != Vd398& Vd396 != Vd398& Vd396 != Vd397& (? [Vd402] :( Vd398 = Vd402& rpoint(Vd402) ))& (? [Vd401] :( Vd397 = Vd401& rpoint(Vd401) ))& (? [Vd400] :( Vd396 = Vd400& rpoint(Vd400) ) ))=> ( rR(Vd397,Vd396,Vd398)| rR(Vd396,Vd397,Vd398)| rR(Vd398,Vd396,Vd397) ) ) )),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f8,axiom,(
% 0.84/0.63 ron(vd1187,vd1232) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f9,axiom,(
% 0.84/0.63 ron(vd1185,vd1197) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f10,axiom,(
% 0.84/0.63 (? [Vd1205] :( vd1201 = Vd1205& rpoint(Vd1205) ) )),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f11,axiom,(
% 0.84/0.63 rline(vd1197) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f12,axiom,(
% 0.84/0.63 ( ~ (? [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.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f14,axiom,(
% 0.84/0.63 ron(vd1201,vd1232) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f20,axiom,(
% 0.84/0.63 vf(vd1178,vd1180) = vf(vd1199,vd1201) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f29,axiom,(
% 0.84/0.63 ron(vd1185,vd1232) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f38,axiom,(
% 0.84/0.63 rS(vd1187,vd1201,vd1197) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f43,axiom,(
% 0.84/0.63 rline(vd1232) ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f45,axiom,(
% 0.84/0.63 vd1199 = vd1185 ),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f55,axiom,(
% 0.84/0.63 (! [Vd748,Vd749] :( ( (? [Vd752] :( Vd749 = Vd752& rpoint(Vd752) ))& (? [Vd751] :( Vd748 = Vd751& rpoint(Vd751) ) ))=> ( vf(Vd748,Vd749) = v0<=> Vd748 = Vd749 ) ) )),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f58,axiom,(
% 0.84/0.63 (! [Vd425,Vd426,Vd430,Vd431] :( ( rS(Vd425,Vd426,Vd430)& Vd430 = Vd431& rline(Vd431)& (? [Vd429] :( Vd426 = Vd429& rpoint(Vd429) ))& (? [Vd428] :( Vd425 = Vd428& rpoint(Vd428) ) ))=> rS(Vd426,Vd425,Vd430) ) )),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f61,axiom,(
% 0.84/0.63 (! [Vd434,Vd435,Vd439,Vd440] :( ( rS(Vd434,Vd435,Vd439)& Vd439 = Vd440& rline(Vd440)& (? [Vd438] :( Vd435 = Vd438& rpoint(Vd438) ))& (? [Vd437] :( Vd434 = Vd437& rpoint(Vd437) ) ))=> ~ ron(Vd434,Vd439) ) )),
% 0.84/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.84/0.63 fof(f160,plain,(
% 0.84/0.63 (~rR(vd1201,vd1185,vd1187)&~rR(vd1187,vd1185,vd1201))),
% 0.84/0.63 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.84/0.63 fof(f161,plain,(
% 0.84/0.63 ~rR(vd1201,vd1185,vd1187)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f160])).
% 0.84/0.63 fof(f162,plain,(
% 0.84/0.63 ~rR(vd1187,vd1185,vd1201)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f160])).
% 0.84/0.63 fof(f163,plain,(
% 0.84/0.63 ~vd1201=vd1187),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f3])).
% 0.84/0.63 fof(f164,plain,(
% 0.84/0.63 ~rR(vd1185,vd1201,vd1187)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f4])).
% 0.84/0.63 fof(f166,plain,(
% 0.84/0.63 ![Vd396,Vd397,Vd398,Vd403,Vd404]: (((((((((((~Vd403=Vd404|~ron(Vd398,Vd403))|~ron(Vd397,Vd403))|~ron(Vd396,Vd403))|~rline(Vd404))|Vd397=Vd398)|Vd396=Vd398)|Vd396=Vd397)|(![Vd402]: (~Vd398=Vd402|~rpoint(Vd402))))|(![Vd401]: (~Vd397=Vd401|~rpoint(Vd401))))|(![Vd400]: (~Vd396=Vd400|~rpoint(Vd400))))|((rR(Vd397,Vd396,Vd398)|rR(Vd396,Vd397,Vd398))|rR(Vd398,Vd396,Vd397)))),
% 0.84/0.63 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.84/0.63 fof(f167,plain,(
% 0.84/0.63 ![Vd396,Vd397,Vd398]: ((((((((![Vd404]: ((![Vd403]: (((~Vd403=Vd404|~ron(Vd398,Vd403))|~ron(Vd397,Vd403))|~ron(Vd396,Vd403)))|~rline(Vd404)))|Vd397=Vd398)|Vd396=Vd398)|Vd396=Vd397)|(![Vd402]: (~Vd398=Vd402|~rpoint(Vd402))))|(![Vd401]: (~Vd397=Vd401|~rpoint(Vd401))))|(![Vd400]: (~Vd396=Vd400|~rpoint(Vd400))))|((rR(Vd397,Vd396,Vd398)|rR(Vd396,Vd397,Vd398))|rR(Vd398,Vd396,Vd397)))),
% 0.84/0.63 inference(miniscoping,[status(thm)],[f166])).
% 0.84/0.63 fof(f168,plain,(
% 0.84/0.63 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~X0=X1|~ron(X2,X0)|~ron(X3,X0)|~ron(X4,X0)|~rline(X1)|X3=X2|X4=X2|X4=X3|~X2=X5|~rpoint(X5)|~X3=X6|~rpoint(X6)|~X4=X7|~rpoint(X7)|rR(X3,X4,X2)|rR(X4,X3,X2)|rR(X2,X4,X3))),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f167])).
% 0.84/0.63 fof(f170,plain,(
% 0.84/0.63 ron(vd1187,vd1232)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f8])).
% 0.84/0.63 fof(f171,plain,(
% 0.84/0.63 ron(vd1185,vd1197)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f9])).
% 0.84/0.63 fof(f172,plain,(
% 0.84/0.63 (vd1201=sK0_skl&rpoint(sK0_skl))),
% 0.84/0.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1205,sK0_skl)],[f10])).
% 0.84/0.63 fof(f173,plain,(
% 0.84/0.63 vd1201=sK0_skl),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f172])).
% 0.84/0.63 fof(f174,plain,(
% 0.84/0.63 rpoint(sK0_skl)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f172])).
% 0.84/0.63 fof(f175,plain,(
% 0.84/0.63 rline(vd1197)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f11])).
% 0.84/0.63 fof(f176,plain,(
% 0.84/0.63 ((((((((((((![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.84/0.63 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.84/0.63 fof(f177,plain,(
% 0.84/0.63 ((((((((((((![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))),
% 0.84/0.63 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)],[f176])).
% 0.84/0.63 fof(f180,plain,(
% 0.84/0.63 vf(vd1178,vd1180)=vf(vd1185,vd1187)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f177])).
% 0.84/0.63 fof(f182,plain,(
% 0.84/0.63 vd1187=sK1_skl),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f177])).
% 0.84/0.63 fof(f183,plain,(
% 0.84/0.63 rpoint(sK1_skl)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f177])).
% 0.84/0.63 fof(f186,plain,(
% 0.84/0.63 vd1185=sK3_skl),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f177])).
% 0.84/0.63 fof(f187,plain,(
% 0.84/0.63 rpoint(sK3_skl)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f177])).
% 0.84/0.63 fof(f200,plain,(
% 0.84/0.63 ron(vd1201,vd1232)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f14])).
% 0.84/0.63 fof(f206,plain,(
% 0.84/0.63 vf(vd1178,vd1180)=vf(vd1199,vd1201)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f20])).
% 0.84/0.63 fof(f219,plain,(
% 0.84/0.63 ron(vd1185,vd1232)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f29])).
% 0.84/0.63 fof(f233,plain,(
% 0.84/0.63 rS(vd1187,vd1201,vd1197)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f38])).
% 0.84/0.63 fof(f238,plain,(
% 0.84/0.63 rline(vd1232)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f43])).
% 0.84/0.63 fof(f240,plain,(
% 0.84/0.63 vd1199=vd1185),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f45])).
% 0.84/0.63 fof(f257,plain,(
% 0.84/0.63 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|(vf(Vd748,Vd749)=v0<=>Vd748=Vd749))),
% 0.84/0.63 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.84/0.63 fof(f258,plain,(
% 0.84/0.63 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|((~vf(Vd748,Vd749)=v0|Vd748=Vd749)&(vf(Vd748,Vd749)=v0|~Vd748=Vd749)))),
% 0.84/0.63 inference(NNF_transformation,[status(thm)],[f257])).
% 0.84/0.63 fof(f259,plain,(
% 0.84/0.63 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|~vf(X2,X0)=v0|X2=X0)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f258])).
% 0.84/0.63 fof(f260,plain,(
% 0.84/0.63 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=v0|~X2=X0)),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f258])).
% 0.84/0.63 fof(f267,plain,(
% 0.84/0.63 ![Vd425,Vd426,Vd430,Vd431]: (((((~rS(Vd425,Vd426,Vd430)|~Vd430=Vd431)|~rline(Vd431))|(![Vd429]: (~Vd426=Vd429|~rpoint(Vd429))))|(![Vd428]: (~Vd425=Vd428|~rpoint(Vd428))))|rS(Vd426,Vd425,Vd430))),
% 0.84/0.63 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.84/0.63 fof(f268,plain,(
% 0.84/0.63 ![Vd425,Vd426,Vd430]: ((((![Vd431]: ((~rS(Vd425,Vd426,Vd430)|~Vd430=Vd431)|~rline(Vd431)))|(![Vd429]: (~Vd426=Vd429|~rpoint(Vd429))))|(![Vd428]: (~Vd425=Vd428|~rpoint(Vd428))))|rS(Vd426,Vd425,Vd430))),
% 0.84/0.63 inference(miniscoping,[status(thm)],[f267])).
% 0.84/0.63 fof(f269,plain,(
% 0.84/0.63 ![X0,X1,X2,X3,X4,X5]: (~rS(X0,X1,X2)|~X2=X3|~rline(X3)|~X1=X4|~rpoint(X4)|~X0=X5|~rpoint(X5)|rS(X1,X0,X2))),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f268])).
% 0.84/0.63 fof(f279,plain,(
% 0.84/0.63 ![Vd434,Vd435,Vd439,Vd440]: (((((~rS(Vd434,Vd435,Vd439)|~Vd439=Vd440)|~rline(Vd440))|(![Vd438]: (~Vd435=Vd438|~rpoint(Vd438))))|(![Vd437]: (~Vd434=Vd437|~rpoint(Vd437))))|~ron(Vd434,Vd439))),
% 0.84/0.63 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.84/0.63 fof(f280,plain,(
% 0.84/0.63 ![Vd434,Vd439]: (((![Vd435]: ((![Vd440]: ((~rS(Vd434,Vd435,Vd439)|~Vd439=Vd440)|~rline(Vd440)))|(![Vd438]: (~Vd435=Vd438|~rpoint(Vd438)))))|(![Vd437]: (~Vd434=Vd437|~rpoint(Vd437))))|~ron(Vd434,Vd439))),
% 0.84/0.63 inference(miniscoping,[status(thm)],[f279])).
% 0.84/0.63 fof(f281,plain,(
% 0.84/0.63 ![X0,X1,X2,X3,X4,X5]: (~rS(X0,X1,X2)|~X2=X3|~rline(X3)|~X1=X4|~rpoint(X4)|~X0=X5|~rpoint(X5)|~ron(X0,X2))),
% 0.84/0.63 inference(cnf_transformation,[status(thm)],[f280])).
% 0.84/0.63 fof(f798,plain,(
% 0.84/0.63 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X2,X1)|~ron(X3,X1)|~rline(X1)|X2=X0|X3=X0|X3=X2|~rpoint(X0)|~rpoint(X2)|~rpoint(X3)|rR(X2,X3,X0)|rR(X3,X2,X0)|rR(X0,X3,X2))),
% 0.84/0.63 inference(destructive_equality_resolution,[status(thm)],[f168])).
% 0.84/0.63 fof(f804,plain,(
% 0.84/0.63 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|~vf(X1,X0)=v0|X1=X0)),
% 0.84/0.63 inference(destructive_equality_resolution,[status(thm)],[f259])).
% 0.84/0.63 fof(f805,plain,(
% 0.84/0.63 ![X1]: (~rpoint(X1)|~rpoint(X1)|vf(X1,X1)=v0)),
% 0.84/0.63 inference(destructive_equality_resolution,[status(thm)],[f260])).
% 0.84/0.63 fof(f806,plain,(
% 0.84/0.63 ![X0]: (~rpoint(X0)|vf(X0,X0)=v0)),
% 0.84/0.63 inference(duplicate_literals_removal,[status(thm)],[f805])).
% 0.84/0.63 fof(f810,plain,(
% 0.84/0.63 ![X0,X1,X2]: (~rS(X0,X1,X2)|~rline(X2)|~rpoint(X1)|~rpoint(X0)|rS(X1,X0,X2))),
% 0.84/0.63 inference(destructive_equality_resolution,[status(thm)],[f269])).
% 0.84/0.63 fof(f815,plain,(
% 0.84/0.63 ![X0,X1,X2]: (~rS(X0,X1,X2)|~rline(X2)|~rpoint(X1)|~rpoint(X0)|~ron(X0,X2))),
% 0.84/0.63 inference(destructive_equality_resolution,[status(thm)],[f281])).
% 0.84/0.63 fof(f1013,plain,(
% 0.84/0.63 rpoint(vd1201)),
% 0.84/0.63 inference(forward_demodulation,[status(thm)],[f173,f174])).
% 0.84/0.63 fof(f1023,definition,(
% 0.84/0.63 sQ15_spl <=> (rline(vd1197))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1025,plain,(
% 0.84/0.63 ~rline(vd1197)|sQ15_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1023])).
% 0.84/0.63 fof(f1026,definition,(
% 0.84/0.63 sQ16_spl <=> (rpoint(vd1185))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1028,plain,(
% 0.84/0.63 ~rpoint(vd1185)|sQ16_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1026])).
% 0.84/0.63 fof(f1033,definition,(
% 0.84/0.63 sQ18_spl <=> (rline(vd1232))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1035,plain,(
% 0.84/0.63 ~rline(vd1232)|sQ18_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1033])).
% 0.84/0.63 fof(f1036,definition,(
% 0.84/0.63 sQ19_spl <=> (rpoint(vd1187))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1037,plain,(
% 0.84/0.63 rpoint(vd1187)|~sQ19_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1036])).
% 0.84/0.63 fof(f1038,plain,(
% 0.84/0.63 ~rpoint(vd1187)|sQ19_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1036])).
% 0.84/0.63 fof(f1040,plain,(
% 0.84/0.63 rpoint(vd1187)),
% 0.84/0.63 inference(forward_demodulation,[status(thm)],[f182,f183])).
% 0.84/0.63 fof(f1041,plain,(
% 0.84/0.63 $false|sQ19_spl),
% 0.84/0.63 inference(forward_subsumption_resolution,[status(thm)],[f1040,f1038])).
% 0.84/0.63 fof(f1042,plain,(
% 0.84/0.63 sQ19_spl),
% 0.84/0.63 inference(contradiction_clause,[status(thm)],[f1041])).
% 0.84/0.63 fof(f1044,plain,(
% 0.84/0.63 rpoint(vd1185)),
% 0.84/0.63 inference(forward_demodulation,[status(thm)],[f186,f187])).
% 0.84/0.63 fof(f1045,plain,(
% 0.84/0.63 $false|sQ16_spl),
% 0.84/0.63 inference(forward_subsumption_resolution,[status(thm)],[f1028,f1044])).
% 0.84/0.63 fof(f1046,plain,(
% 0.84/0.63 sQ16_spl),
% 0.84/0.63 inference(contradiction_clause,[status(thm)],[f1045])).
% 0.84/0.63 fof(f1058,plain,(
% 0.84/0.63 ![X0,X1]: (~ron(X0,vd1232)|~ron(X1,vd1232)|~rline(vd1232)|X0=vd1187|X1=vd1187|X1=X0|~rpoint(vd1187)|~rpoint(X0)|~rpoint(X1)|rR(X0,X1,vd1187)|rR(X1,X0,vd1187)|rR(vd1187,X1,X0))),
% 0.84/0.63 inference(resolution,[status(thm)],[f798,f170])).
% 0.84/0.63 fof(f1063,definition,(
% 0.84/0.63 ![X0,X1]: (sQ23_spl <=> (~ron(X0,vd1232)|~ron(X1,vd1232)|X0=vd1187|X1=vd1187|X1=X0|~rpoint(X0)|~rpoint(X1)|rR(X0,X1,vd1187)|rR(X1,X0,vd1187)|rR(vd1187,X1,X0)))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1064,plain,(
% 0.84/0.63 ![X0,X1]: (~ron(X0,vd1232)|~ron(X1,vd1232)|X0=vd1187|X1=vd1187|X1=X0|~rpoint(X0)|~rpoint(X1)|rR(X0,X1,vd1187)|rR(X1,X0,vd1187)|rR(vd1187,X1,X0)|~sQ23_spl)),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1063])).
% 0.84/0.63 fof(f1066,plain,(
% 0.84/0.63 sQ23_spl|~sQ18_spl|~sQ19_spl),
% 0.84/0.63 inference(split_clause,[status(thm)],[f1058,f1063,f1033,f1036])).
% 0.84/0.63 fof(f1087,definition,(
% 0.84/0.63 sQ27_spl <=> (rpoint(vd1201))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1089,plain,(
% 0.84/0.63 ~rpoint(vd1201)|sQ27_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1087])).
% 0.84/0.63 fof(f1114,definition,(
% 0.84/0.63 sQ32_spl <=> (ron(vd1185,vd1197))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1116,plain,(
% 0.84/0.63 ~ron(vd1185,vd1197)|sQ32_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1114])).
% 0.84/0.63 fof(f1161,plain,(
% 0.84/0.63 $false|sQ18_spl),
% 0.84/0.63 inference(forward_subsumption_resolution,[status(thm)],[f238,f1035])).
% 0.84/0.63 fof(f1162,plain,(
% 0.84/0.63 sQ18_spl),
% 0.84/0.63 inference(contradiction_clause,[status(thm)],[f1161])).
% 0.84/0.63 fof(f1163,plain,(
% 0.84/0.63 $false|sQ27_spl),
% 0.84/0.63 inference(forward_subsumption_resolution,[status(thm)],[f1089,f1013])).
% 0.84/0.63 fof(f1164,plain,(
% 0.84/0.63 sQ27_spl),
% 0.84/0.63 inference(contradiction_clause,[status(thm)],[f1163])).
% 0.84/0.63 fof(f1171,plain,(
% 0.84/0.63 vf(vd1185,vd1187)=vf(vd1199,vd1201)),
% 0.84/0.63 inference(forward_demodulation,[status(thm)],[f180,f206])).
% 0.84/0.63 fof(f1173,plain,(
% 0.84/0.63 vf(vd1185,vd1187)=vf(vd1185,vd1201)),
% 0.84/0.63 inference(forward_demodulation,[status(thm)],[f240,f1171])).
% 0.84/0.63 fof(f1177,plain,(
% 0.84/0.63 ![X0]: (~ron(X0,vd1232)|vd1201=vd1187|X0=vd1187|X0=vd1201|~rpoint(vd1201)|~rpoint(X0)|rR(vd1201,X0,vd1187)|rR(X0,vd1201,vd1187)|rR(vd1187,X0,vd1201)|~sQ23_spl)),
% 0.84/0.63 inference(resolution,[status(thm)],[f1064,f200])).
% 0.84/0.63 fof(f1179,definition,(
% 0.84/0.63 ![X0]: (sQ43_spl <=> (~ron(X0,vd1232)|X0=vd1187|X0=vd1201|~rpoint(X0)|rR(vd1201,X0,vd1187)|rR(X0,vd1201,vd1187)|rR(vd1187,X0,vd1201)))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1180,plain,(
% 0.84/0.63 ![X0]: (~ron(X0,vd1232)|X0=vd1187|X0=vd1201|~rpoint(X0)|rR(vd1201,X0,vd1187)|rR(X0,vd1201,vd1187)|rR(vd1187,X0,vd1201)|~sQ43_spl)),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1179])).
% 0.84/0.63 fof(f1182,definition,(
% 0.84/0.63 sQ44_spl <=> (vd1201=vd1187)),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1183,plain,(
% 0.84/0.63 vd1201=vd1187|~sQ44_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1182])).
% 0.84/0.63 fof(f1185,plain,(
% 0.84/0.63 sQ43_spl|sQ44_spl|~sQ27_spl|~sQ23_spl),
% 0.84/0.63 inference(split_clause,[status(thm)],[f1177,f1179,f1182,f1087,f1063])).
% 0.84/0.63 fof(f1207,plain,(
% 0.84/0.63 $false|~sQ44_spl),
% 0.84/0.63 inference(forward_subsumption_resolution,[status(thm)],[f1183,f163])).
% 0.84/0.63 fof(f1208,plain,(
% 0.84/0.63 ~sQ44_spl),
% 0.84/0.63 inference(contradiction_clause,[status(thm)],[f1207])).
% 0.84/0.63 fof(f1210,plain,(
% 0.84/0.63 $false|sQ15_spl),
% 0.84/0.63 inference(forward_subsumption_resolution,[status(thm)],[f175,f1025])).
% 0.84/0.63 fof(f1211,plain,(
% 0.84/0.63 sQ15_spl),
% 0.84/0.63 inference(contradiction_clause,[status(thm)],[f1210])).
% 0.84/0.63 fof(f1273,definition,(
% 0.84/0.63 sQ58_spl <=> (vd1185=vd1201)),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1274,plain,(
% 0.84/0.63 vd1185=vd1201|~sQ58_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1273])).
% 0.84/0.63 fof(f1280,definition,(
% 0.84/0.63 sQ60_spl <=> (vd1185=vd1187)),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1281,plain,(
% 0.84/0.63 vd1185=vd1187|~sQ60_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1280])).
% 0.84/0.63 fof(f1410,plain,(
% 0.84/0.63 vf(vd1185,vd1187)=vf(vd1201,vd1201)|~sQ58_spl),
% 0.84/0.63 inference(backward_demodulation,[status(thm)],[f1274,f1173])).
% 0.84/0.63 fof(f1427,plain,(
% 0.84/0.63 vf(vd1201,vd1187)=vf(vd1201,vd1201)|~sQ58_spl),
% 0.84/0.63 inference(forward_demodulation,[status(thm)],[f1274,f1410])).
% 0.84/0.63 fof(f1487,plain,(
% 0.84/0.63 ![X0]: (~rpoint(X0)|~vf(X0,vd1187)=v0|X0=vd1187|~sQ19_spl)),
% 0.84/0.63 inference(resolution,[status(thm)],[f804,f1037])).
% 0.84/0.63 fof(f1495,plain,(
% 0.84/0.63 ~vf(vd1201,vd1187)=v0|vd1201=vd1187|~sQ19_spl),
% 0.84/0.63 inference(resolution,[status(thm)],[f1487,f1013])).
% 0.84/0.63 fof(f1535,definition,(
% 0.84/0.63 sQ94_spl <=> (vf(vd1201,vd1187)=v0)),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1537,plain,(
% 0.84/0.63 ~vf(vd1201,vd1187)=v0|sQ94_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1535])).
% 0.84/0.63 fof(f1538,plain,(
% 0.84/0.63 ~sQ94_spl|sQ44_spl|~sQ19_spl),
% 0.84/0.63 inference(split_clause,[status(thm)],[f1495,f1535,f1182,f1036])).
% 0.84/0.63 fof(f1551,plain,(
% 0.84/0.63 rS(vd1185,vd1201,vd1197)|~sQ60_spl),
% 0.84/0.63 inference(backward_demodulation,[status(thm)],[f1281,f233])).
% 0.84/0.63 fof(f1565,plain,(
% 0.84/0.63 vf(vd1185,vd1185)=v0),
% 0.84/0.63 inference(resolution,[status(thm)],[f806,f1044])).
% 0.84/0.63 fof(f1594,plain,(
% 0.84/0.63 ~rline(vd1197)|~rpoint(vd1201)|~rpoint(vd1185)|rS(vd1201,vd1185,vd1197)|~sQ60_spl),
% 0.84/0.63 inference(resolution,[status(thm)],[f810,f1551])).
% 0.84/0.63 fof(f1595,definition,(
% 0.84/0.63 sQ96_spl <=> (rS(vd1201,vd1185,vd1197))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1596,plain,(
% 0.84/0.63 rS(vd1201,vd1185,vd1197)|~sQ96_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1595])).
% 0.84/0.63 fof(f1598,plain,(
% 0.84/0.63 ~sQ15_spl|~sQ27_spl|~sQ16_spl|sQ96_spl|~sQ60_spl),
% 0.84/0.63 inference(split_clause,[status(thm)],[f1594,f1023,f1087,f1026,f1595,f1280])).
% 0.84/0.63 fof(f1885,plain,(
% 0.84/0.63 ~rline(vd1197)|~rpoint(vd1185)|~rpoint(vd1201)|rS(vd1185,vd1201,vd1197)|~sQ96_spl),
% 0.84/0.63 inference(resolution,[status(thm)],[f1596,f810])).
% 0.84/0.63 fof(f1890,definition,(
% 0.84/0.63 sQ142_spl <=> (rS(vd1185,vd1201,vd1197))),
% 0.84/0.63 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 0.84/0.63 fof(f1891,plain,(
% 0.84/0.63 rS(vd1185,vd1201,vd1197)|~sQ142_spl),
% 0.84/0.63 inference(component_clause,[status(thm)],[f1890])).
% 0.84/0.63 fof(f1893,plain,(
% 0.84/0.63 ~sQ15_spl|~sQ16_spl|~sQ27_spl|sQ142_spl|~sQ96_spl),
% 0.84/0.63 inference(split_clause,[status(thm)],[f1885,f1023,f1026,f1087,f1890,f1595])).
% 0.84/0.63 fof(f2088,plain,(
% 0.84/0.63 ~rline(vd1197)|~rpoint(vd1201)|~rpoint(vd1185)|~ron(vd1185,vd1197)|~sQ142_spl),
% 0.84/0.63 inference(resolution,[status(thm)],[f1891,f815])).
% 0.84/0.63 fof(f2090,plain,(
% 0.84/0.63 ~sQ15_spl|~sQ27_spl|~sQ16_spl|~sQ32_spl|~sQ142_spl),
% 0.84/0.63 inference(split_clause,[status(thm)],[f2088,f1023,f1087,f1026,f1114,f1890])).
% 0.84/0.63 fof(f2092,plain,(
% 0.84/0.63 $false|sQ32_spl),
% 0.84/0.63 inference(forward_subsumption_resolution,[status(thm)],[f1116,f171])).
% 0.84/0.63 fof(f2093,plain,(
% 0.84/0.63 sQ32_spl),
% 0.84/0.63 inference(contradiction_clause,[status(thm)],[f2092])).
% 0.84/0.63 fof(f2125,plain,(
% 0.84/0.63 vd1185=vd1187|vd1185=vd1201|~rpoint(vd1185)|rR(vd1201,vd1185,vd1187)|rR(vd1185,vd1201,vd1187)|rR(vd1187,vd1185,vd1201)|~sQ43_spl),
% 0.84/0.63 inference(resolution,[status(thm)],[f1180,f219])).
% 0.84/0.63 fof(f2137,definition,(
% 0.84/0.63 sQ182_spl <=> (rR(vd1201,vd1185,vd1187))),
% 0.84/0.64 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 0.84/0.64 fof(f2138,plain,(
% 0.84/0.64 rR(vd1201,vd1185,vd1187)|~sQ182_spl),
% 0.84/0.64 inference(component_clause,[status(thm)],[f2137])).
% 0.84/0.64 fof(f2140,definition,(
% 0.84/0.64 sQ183_spl <=> (rR(vd1185,vd1201,vd1187))),
% 0.84/0.64 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 0.84/0.64 fof(f2141,plain,(
% 0.84/0.64 rR(vd1185,vd1201,vd1187)|~sQ183_spl),
% 0.84/0.64 inference(component_clause,[status(thm)],[f2140])).
% 0.84/0.64 fof(f2143,definition,(
% 0.84/0.64 sQ184_spl <=> (rR(vd1187,vd1185,vd1201))),
% 0.84/0.64 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 0.84/0.64 fof(f2144,plain,(
% 0.84/0.64 rR(vd1187,vd1185,vd1201)|~sQ184_spl),
% 0.84/0.64 inference(component_clause,[status(thm)],[f2143])).
% 0.84/0.64 fof(f2146,plain,(
% 0.84/0.64 sQ60_spl|sQ58_spl|~sQ16_spl|sQ182_spl|sQ183_spl|sQ184_spl|~sQ43_spl),
% 0.84/0.64 inference(split_clause,[status(thm)],[f2125,f1280,f1273,f1026,f2137,f2140,f2143,f1179])).
% 0.84/0.64 fof(f2211,plain,(
% 0.84/0.64 ~vf(vd1201,vd1201)=v0|~sQ58_spl|sQ94_spl),
% 0.84/0.64 inference(backward_demodulation,[status(thm)],[f1427,f1537])).
% 0.84/0.64 fof(f3515,plain,(
% 0.84/0.64 vf(vd1201,vd1185)=v0|~sQ58_spl),
% 0.84/0.64 inference(forward_demodulation,[status(thm)],[f1274,f1565])).
% 0.84/0.64 fof(f3516,plain,(
% 0.84/0.64 vf(vd1201,vd1201)=v0|~sQ58_spl),
% 0.84/0.64 inference(forward_demodulation,[status(thm)],[f1274,f3515])).
% 0.84/0.64 fof(f3517,plain,(
% 0.84/0.64 $false|sQ94_spl|~sQ58_spl),
% 0.84/0.64 inference(forward_subsumption_resolution,[status(thm)],[f3516,f2211])).
% 0.84/0.64 fof(f3518,plain,(
% 0.84/0.64 sQ94_spl|~sQ58_spl),
% 0.84/0.64 inference(contradiction_clause,[status(thm)],[f3517])).
% 0.84/0.64 fof(f4267,plain,(
% 0.84/0.64 $false|~sQ184_spl),
% 0.84/0.64 inference(forward_subsumption_resolution,[status(thm)],[f2144,f162])).
% 0.84/0.64 fof(f4268,plain,(
% 0.84/0.64 ~sQ184_spl),
% 0.84/0.64 inference(contradiction_clause,[status(thm)],[f4267])).
% 0.84/0.64 fof(f4269,plain,(
% 0.84/0.64 $false|~sQ182_spl),
% 0.84/0.64 inference(forward_subsumption_resolution,[status(thm)],[f2138,f161])).
% 0.84/0.64 fof(f4270,plain,(
% 0.84/0.64 ~sQ182_spl),
% 0.84/0.64 inference(contradiction_clause,[status(thm)],[f4269])).
% 0.84/0.64 fof(f4271,plain,(
% 0.84/0.64 $false|~sQ183_spl),
% 0.84/0.64 inference(forward_subsumption_resolution,[status(thm)],[f2141,f164])).
% 0.84/0.64 fof(f4272,plain,(
% 0.84/0.64 ~sQ183_spl),
% 0.84/0.64 inference(contradiction_clause,[status(thm)],[f4271])).
% 0.84/0.64 fof(f4273,plain,(
% 0.84/0.64 $false),
% 0.84/0.64 inference(sat_refutation,[status(thm)],[f1042,f1046,f1066,f1162,f1164,f1185,f1208,f1211,f1538,f1598,f1893,f2090,f2093,f2146,f3518,f4268,f4270,f4272])).
% 0.84/0.64 % SZS output end CNFRefutation for theBenchmark.p
% 0.84/0.66 % Elapsed time: 0.295456 seconds
% 0.84/0.66 % CPU time: 1.865113 seconds
% 0.84/0.66 % Total memory used: 135.005 MB
% 0.84/0.66 % Net memory used: 132.862 MB
%------------------------------------------------------------------------------