%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO290+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 : 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:20 PM UTC 2026
% Result : Theorem 2.28s 0.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO290+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n003.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:11:30 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 2.28/0.75 % Refutation found
% 2.28/0.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.28/0.75 % SZS output start CNFRefutation for theBenchmark
% 2.28/0.75 fof(f1,conjecture,(
% 2.28/0.75 ( rR(vd1199,vd1185,vd1186)| rR(vd1185,vd1199,vd1186) ) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f2,negated_conjecture,(
% 2.28/0.75 ~(( rR(vd1199,vd1185,vd1186)| rR(vd1185,vd1199,vd1186) ) )),
% 2.28/0.75 inference(negated_conjecture,[status(cth)],[f1])).
% 2.28/0.75 fof(f3,axiom,(
% 2.28/0.75 vd1199 != vd1185 ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f4,axiom,(
% 2.28/0.75 ron(vd1185,vd1197) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f5,axiom,(
% 2.28/0.75 ron(vd1200,vd1197) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f7,axiom,(
% 2.28/0.75 ron(vd1199,vd1197) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f8,axiom,(
% 2.28/0.75 vd1200 = vd1186 ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f10,axiom,(
% 2.28/0.75 (! [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) ) ) )),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f11,axiom,(
% 2.28/0.75 vf(vd1199,vd1200) = vf(vd1185,vd1186) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f13,axiom,(
% 2.28/0.75 rline(vd1197) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f15,axiom,(
% 2.28/0.75 ~ rR(vd1186,vd1199,vd1185) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f24,axiom,(
% 2.28/0.75 (? [Vd1204] :( vd1200 = Vd1204& rpoint(Vd1204) ) )),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f25,axiom,(
% 2.28/0.75 (? [Vd1203] :( vd1199 = Vd1203& rpoint(Vd1203) ) )),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f27,axiom,(
% 2.28/0.75 ( ~ (? [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) ) )) ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f31,axiom,(
% 2.28/0.75 (! [Vd748,Vd749] :( ( (? [Vd752] :( Vd749 = Vd752& rpoint(Vd752) ))& (? [Vd751] :( Vd748 = Vd751& rpoint(Vd751) ) ))=> ( vf(Vd748,Vd749) = v0<=> Vd748 = Vd749 ) ) )),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f69,axiom,(
% 2.28/0.75 v0 = vd684 ),
% 2.28/0.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.28/0.75 fof(f137,plain,(
% 2.28/0.75 (~rR(vd1199,vd1185,vd1186)&~rR(vd1185,vd1199,vd1186))),
% 2.28/0.75 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 2.28/0.75 fof(f138,plain,(
% 2.28/0.75 ~rR(vd1199,vd1185,vd1186)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f137])).
% 2.28/0.75 fof(f139,plain,(
% 2.28/0.75 ~rR(vd1185,vd1199,vd1186)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f137])).
% 2.28/0.75 fof(f140,plain,(
% 2.28/0.75 ~vd1199=vd1185),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f3])).
% 2.28/0.75 fof(f141,plain,(
% 2.28/0.75 ron(vd1185,vd1197)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f4])).
% 2.28/0.75 fof(f142,plain,(
% 2.28/0.75 ron(vd1200,vd1197)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f5])).
% 2.28/0.75 fof(f144,plain,(
% 2.28/0.75 ron(vd1199,vd1197)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f7])).
% 2.28/0.75 fof(f145,plain,(
% 2.28/0.75 vd1200=vd1186),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f8])).
% 2.28/0.75 fof(f147,plain,(
% 2.28/0.75 ![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)))),
% 2.28/0.75 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 2.28/0.75 fof(f148,plain,(
% 2.28/0.75 ![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)))),
% 2.28/0.75 inference(miniscoping,[status(thm)],[f147])).
% 2.28/0.75 fof(f149,plain,(
% 2.28/0.75 ![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))),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f148])).
% 2.28/0.75 fof(f150,plain,(
% 2.28/0.75 vf(vd1199,vd1200)=vf(vd1185,vd1186)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f11])).
% 2.28/0.75 fof(f152,plain,(
% 2.28/0.75 rline(vd1197)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f13])).
% 2.28/0.75 fof(f154,plain,(
% 2.28/0.75 ~rR(vd1186,vd1199,vd1185)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f15])).
% 2.28/0.75 fof(f165,plain,(
% 2.28/0.75 (vd1200=sK1_skl&rpoint(sK1_skl))),
% 2.28/0.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd1204,sK1_skl)],[f24])).
% 2.28/0.75 fof(f166,plain,(
% 2.28/0.75 vd1200=sK1_skl),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f165])).
% 2.28/0.75 fof(f167,plain,(
% 2.28/0.75 rpoint(sK1_skl)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f165])).
% 2.28/0.75 fof(f168,plain,(
% 2.28/0.75 (vd1199=sK2_skl&rpoint(sK2_skl))),
% 2.28/0.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd1203,sK2_skl)],[f25])).
% 2.28/0.75 fof(f169,plain,(
% 2.28/0.75 vd1199=sK2_skl),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f168])).
% 2.28/0.75 fof(f170,plain,(
% 2.28/0.75 rpoint(sK2_skl)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f168])).
% 2.28/0.75 fof(f172,plain,(
% 2.28/0.75 ((((((((((((![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)))),
% 2.28/0.75 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 2.28/0.75 fof(f173,plain,(
% 2.28/0.75 ((((((((((((![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=sK3_skl&rpoint(sK3_skl)))&(vd1186=sK4_skl&rpoint(sK4_skl)))&(vd1185=sK5_skl&rpoint(sK5_skl)))&~vd1179=vd1180)&~vd1178=vd1180)&~vd1178=vd1179)&(vd1180=sK6_skl&rpoint(sK6_skl)))&(vd1179=sK7_skl&rpoint(sK7_skl)))&(vd1178=sK8_skl&rpoint(sK8_skl))),
% 2.28/0.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(Vd1191,sK3_skl),skolemize(Vd1190,sK4_skl),skolemize(Vd1189,sK5_skl),skolemize(Vd1184,sK6_skl),skolemize(Vd1183,sK7_skl),skolemize(Vd1182,sK8_skl)],[f172])).
% 2.28/0.75 fof(f177,plain,(
% 2.28/0.75 vf(vd1178,vd1179)=vf(vd1185,vd1186)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f182,plain,(
% 2.28/0.75 vd1185=sK5_skl),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f183,plain,(
% 2.28/0.75 rpoint(sK5_skl)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f186,plain,(
% 2.28/0.75 ~vd1178=vd1179),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f189,plain,(
% 2.28/0.75 vd1179=sK7_skl),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f190,plain,(
% 2.28/0.75 rpoint(sK7_skl)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f191,plain,(
% 2.28/0.75 vd1178=sK8_skl),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f192,plain,(
% 2.28/0.75 rpoint(sK8_skl)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f173])).
% 2.28/0.75 fof(f199,plain,(
% 2.28/0.75 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|(vf(Vd748,Vd749)=v0<=>Vd748=Vd749))),
% 2.28/0.75 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 2.28/0.75 fof(f200,plain,(
% 2.28/0.75 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|((~vf(Vd748,Vd749)=v0|Vd748=Vd749)&(vf(Vd748,Vd749)=v0|~Vd748=Vd749)))),
% 2.28/0.75 inference(NNF_transformation,[status(thm)],[f199])).
% 2.28/0.75 fof(f201,plain,(
% 2.28/0.75 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|~vf(X2,X0)=v0|X2=X0)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f200])).
% 2.28/0.75 fof(f202,plain,(
% 2.28/0.75 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=v0|~X2=X0)),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f200])).
% 2.28/0.75 fof(f345,plain,(
% 2.28/0.75 v0=vd684),
% 2.28/0.75 inference(cnf_transformation,[status(thm)],[f69])).
% 2.28/0.75 fof(f720,plain,(
% 2.28/0.75 ![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))),
% 2.28/0.75 inference(destructive_equality_resolution,[status(thm)],[f149])).
% 2.28/0.75 fof(f724,plain,(
% 2.28/0.75 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|~vf(X1,X0)=v0|X1=X0)),
% 2.28/0.75 inference(destructive_equality_resolution,[status(thm)],[f201])).
% 2.28/0.75 fof(f725,plain,(
% 2.28/0.75 ![X1]: (~rpoint(X1)|~rpoint(X1)|vf(X1,X1)=v0)),
% 2.28/0.75 inference(destructive_equality_resolution,[status(thm)],[f202])).
% 2.28/0.75 fof(f726,plain,(
% 2.28/0.75 ![X0]: (~rpoint(X0)|vf(X0,X0)=v0)),
% 2.28/0.75 inference(duplicate_literals_removal,[status(thm)],[f725])).
% 2.28/0.75 fof(f941,plain,(
% 2.28/0.75 vf(vd1178,vd1179)=vf(vd1185,vd1200)),
% 2.28/0.75 inference(backward_demodulation,[status(thm)],[f145,f177])).
% 2.28/0.75 fof(f942,plain,(
% 2.28/0.75 ~rR(vd1200,vd1199,vd1185)),
% 2.28/0.75 inference(backward_demodulation,[status(thm)],[f145,f154])).
% 2.28/0.75 fof(f944,plain,(
% 2.28/0.75 ~rR(vd1185,vd1199,vd1200)),
% 2.28/0.75 inference(backward_demodulation,[status(thm)],[f145,f139])).
% 2.28/0.75 fof(f945,plain,(
% 2.28/0.75 ~rR(vd1199,vd1185,vd1200)),
% 2.28/0.75 inference(backward_demodulation,[status(thm)],[f145,f138])).
% 2.28/0.75 fof(f956,plain,(
% 2.28/0.75 rpoint(vd1200)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f166,f167])).
% 2.28/0.75 fof(f962,plain,(
% 2.28/0.75 rpoint(vd1199)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f169,f170])).
% 2.28/0.75 fof(f976,plain,(
% 2.28/0.75 rpoint(vd1185)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f182,f183])).
% 2.28/0.75 fof(f982,plain,(
% 2.28/0.75 vf(vd1199,vd1200)=vf(vd1185,vd1200)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f145,f150])).
% 2.28/0.75 fof(f983,plain,(
% 2.28/0.75 vf(vd1199,vd1200)=vf(vd1178,vd1179)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f941,f982])).
% 2.28/0.75 fof(f990,plain,(
% 2.28/0.75 rpoint(vd1179)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f189,f190])).
% 2.28/0.75 fof(f996,plain,(
% 2.28/0.75 rpoint(vd1178)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f191,f192])).
% 2.28/0.75 fof(f1007,plain,(
% 2.28/0.75 ![X0,X1,X2]: (~ron(X0,vd1197)|~ron(X1,vd1197)|~ron(X2,vd1197)|X1=X0|X2=X0|X2=X1|~rpoint(X0)|~rpoint(X1)|~rpoint(X2)|rR(X1,X2,X0)|rR(X2,X1,X0)|rR(X0,X2,X1))),
% 2.28/0.75 inference(resolution,[status(thm)],[f152,f720])).
% 2.28/0.75 fof(f1026,plain,(
% 2.28/0.75 ![X0,X1]: (~ron(X0,vd1197)|~ron(X1,vd1197)|vd1185=X0|X1=X0|X1=vd1185|~rpoint(X0)|~rpoint(vd1185)|~rpoint(X1)|rR(vd1185,X1,X0)|rR(X1,vd1185,X0)|rR(X0,X1,vd1185))),
% 2.28/0.75 inference(resolution,[status(thm)],[f1007,f141])).
% 2.28/0.75 fof(f1036,definition,(
% 2.28/0.75 sQ10_spl <=> (rpoint(vd1199))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1038,plain,(
% 2.28/0.75 ~rpoint(vd1199)|sQ10_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1036])).
% 2.28/0.75 fof(f1050,definition,(
% 2.28/0.75 sQ14_spl <=> (rpoint(vd1200))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1052,plain,(
% 2.28/0.75 ~rpoint(vd1200)|sQ14_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1050])).
% 2.28/0.75 fof(f1064,definition,(
% 2.28/0.75 sQ18_spl <=> (rpoint(vd1185))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1066,plain,(
% 2.28/0.75 ~rpoint(vd1185)|sQ18_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1064])).
% 2.28/0.75 fof(f1068,definition,(
% 2.28/0.75 ![X0,X1]: (sQ19_spl <=> (~ron(X0,vd1197)|~ron(X1,vd1197)|vd1185=X0|X1=X0|X1=vd1185|~rpoint(X0)|~rpoint(X1)|rR(vd1185,X1,X0)|rR(X1,vd1185,X0)|rR(X0,X1,vd1185)))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1069,plain,(
% 2.28/0.75 ![X0,X1]: (~ron(X0,vd1197)|~ron(X1,vd1197)|vd1185=X0|X1=X0|X1=vd1185|~rpoint(X0)|~rpoint(X1)|rR(vd1185,X1,X0)|rR(X1,vd1185,X0)|rR(X0,X1,vd1185)|~sQ19_spl)),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1068])).
% 2.28/0.75 fof(f1071,plain,(
% 2.28/0.75 sQ19_spl|~sQ18_spl),
% 2.28/0.75 inference(split_clause,[status(thm)],[f1026,f1068,f1064])).
% 2.28/0.75 fof(f1084,plain,(
% 2.28/0.75 $false|sQ18_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1066,f976])).
% 2.28/0.75 fof(f1085,plain,(
% 2.28/0.75 sQ18_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f1084])).
% 2.28/0.75 fof(f1086,plain,(
% 2.28/0.75 $false|sQ14_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1052,f956])).
% 2.28/0.75 fof(f1087,plain,(
% 2.28/0.75 sQ14_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f1086])).
% 2.28/0.75 fof(f1088,plain,(
% 2.28/0.75 $false|sQ10_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1038,f962])).
% 2.28/0.75 fof(f1089,plain,(
% 2.28/0.75 sQ10_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f1088])).
% 2.28/0.75 fof(f1132,definition,(
% 2.28/0.75 sQ26_spl <=> (rpoint(vd1179))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1134,plain,(
% 2.28/0.75 ~rpoint(vd1179)|sQ26_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1132])).
% 2.28/0.75 fof(f1149,definition,(
% 2.28/0.75 sQ31_spl <=> (vd1199=vd1200)),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1150,plain,(
% 2.28/0.75 vd1199=vd1200|~sQ31_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1149])).
% 2.28/0.75 fof(f1166,definition,(
% 2.28/0.75 sQ36_spl <=> (vd1185=vd1200)),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1167,plain,(
% 2.28/0.75 vd1185=vd1200|~sQ36_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1166])).
% 2.28/0.75 fof(f1194,plain,(
% 2.28/0.75 $false|sQ26_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1134,f990])).
% 2.28/0.75 fof(f1195,plain,(
% 2.28/0.75 sQ26_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f1194])).
% 2.28/0.75 fof(f1212,plain,(
% 2.28/0.75 vf(vd1178,vd1179)=vf(vd1200,vd1200)|~sQ36_spl),
% 2.28/0.75 inference(backward_demodulation,[status(thm)],[f1167,f941])).
% 2.28/0.75 fof(f1233,definition,(
% 2.28/0.75 sQ44_spl <=> (rpoint(vd1178))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1235,plain,(
% 2.28/0.75 ~rpoint(vd1178)|sQ44_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1233])).
% 2.28/0.75 fof(f1241,plain,(
% 2.28/0.75 $false|sQ44_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1235,f996])).
% 2.28/0.75 fof(f1242,plain,(
% 2.28/0.75 sQ44_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f1241])).
% 2.28/0.75 fof(f1253,plain,(
% 2.28/0.75 vf(vd1200,vd1200)=vf(vd1178,vd1179)|~sQ31_spl),
% 2.28/0.75 inference(backward_demodulation,[status(thm)],[f1150,f983])).
% 2.28/0.75 fof(f1299,plain,(
% 2.28/0.75 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|~vf(X1,X0)=vd684|X1=X0)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f345,f724])).
% 2.28/0.75 fof(f1340,definition,(
% 2.28/0.75 sQ51_spl <=> (vd1178=vd1179)),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1341,plain,(
% 2.28/0.75 vd1178=vd1179|~sQ51_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1340])).
% 2.28/0.75 fof(f1368,plain,(
% 2.28/0.75 $false|~sQ51_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f1341,f186])).
% 2.28/0.75 fof(f1369,plain,(
% 2.28/0.75 ~sQ51_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f1368])).
% 2.28/0.75 fof(f1425,plain,(
% 2.28/0.75 ![X0]: (~rpoint(X0)|vf(X0,X0)=vd684)),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f345,f726])).
% 2.28/0.75 fof(f1426,plain,(
% 2.28/0.75 vf(vd1200,vd1200)=vd684),
% 2.28/0.75 inference(resolution,[status(thm)],[f1425,f956])).
% 2.28/0.75 fof(f1533,definition,(
% 2.28/0.75 sQ70_spl <=> (vf(vd1178,vd1179)=vd684)),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f1535,plain,(
% 2.28/0.75 ~vf(vd1178,vd1179)=vd684|sQ70_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f1533])).
% 2.28/0.75 fof(f1562,plain,(
% 2.28/0.75 ~rpoint(vd1200)|~rpoint(vd1185)|~vf(vd1178,vd1179)=vd684|vd1185=vd1200),
% 2.28/0.75 inference(paramodulation,[status(thm)],[f941,f1299])).
% 2.28/0.75 fof(f1569,plain,(
% 2.28/0.75 ~sQ14_spl|~sQ18_spl|~sQ70_spl|sQ36_spl),
% 2.28/0.75 inference(split_clause,[status(thm)],[f1562,f1050,f1064,f1533,f1166])).
% 2.28/0.75 fof(f2024,plain,(
% 2.28/0.75 vf(vd1178,vd1179)=vd684|~sQ36_spl),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f1426,f1212])).
% 2.28/0.75 fof(f2025,plain,(
% 2.28/0.75 ~rpoint(vd1179)|~rpoint(vd1178)|vd1178=vd1179|~sQ36_spl),
% 2.28/0.75 inference(resolution,[status(thm)],[f2024,f1299])).
% 2.28/0.75 fof(f2033,plain,(
% 2.28/0.75 ~sQ26_spl|~sQ44_spl|sQ51_spl|~sQ36_spl),
% 2.28/0.75 inference(split_clause,[status(thm)],[f2025,f1132,f1233,f1340,f1166])).
% 2.28/0.75 fof(f2059,plain,(
% 2.28/0.75 vd684=vf(vd1178,vd1179)|~sQ31_spl),
% 2.28/0.75 inference(forward_demodulation,[status(thm)],[f1426,f1253])).
% 2.28/0.75 fof(f2704,definition,(
% 2.28/0.75 sQ217_spl <=> (vd1185=vd1199)),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f2705,plain,(
% 2.28/0.75 vd1185=vd1199|~sQ217_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f2704])).
% 2.28/0.75 fof(f2719,plain,(
% 2.28/0.75 $false|~sQ217_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f2705,f140])).
% 2.28/0.75 fof(f2720,plain,(
% 2.28/0.75 ~sQ217_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f2719])).
% 2.28/0.75 fof(f2816,plain,(
% 2.28/0.75 $false|sQ70_spl|~sQ31_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f2059,f1535])).
% 2.28/0.75 fof(f2817,plain,(
% 2.28/0.75 sQ70_spl|~sQ31_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f2816])).
% 2.28/0.75 fof(f3703,plain,(
% 2.28/0.75 ![X0]: (~ron(X0,vd1197)|vd1185=X0|vd1199=X0|vd1199=vd1185|~rpoint(X0)|~rpoint(vd1199)|rR(vd1185,vd1199,X0)|rR(vd1199,vd1185,X0)|rR(X0,vd1199,vd1185)|~sQ19_spl)),
% 2.28/0.75 inference(resolution,[status(thm)],[f1069,f144])).
% 2.28/0.75 fof(f3710,definition,(
% 2.28/0.75 ![X0]: (sQ382_spl <=> (~ron(X0,vd1197)|vd1185=X0|vd1199=X0|~rpoint(X0)|rR(vd1185,vd1199,X0)|rR(vd1199,vd1185,X0)|rR(X0,vd1199,vd1185)))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ382_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f3711,plain,(
% 2.28/0.75 ![X0]: (~ron(X0,vd1197)|vd1185=X0|vd1199=X0|~rpoint(X0)|rR(vd1185,vd1199,X0)|rR(vd1199,vd1185,X0)|rR(X0,vd1199,vd1185)|~sQ382_spl)),
% 2.28/0.75 inference(component_clause,[status(thm)],[f3710])).
% 2.28/0.75 fof(f3713,plain,(
% 2.28/0.75 sQ382_spl|sQ217_spl|~sQ10_spl|~sQ19_spl),
% 2.28/0.75 inference(split_clause,[status(thm)],[f3703,f3710,f2704,f1036,f1068])).
% 2.28/0.75 fof(f3721,plain,(
% 2.28/0.75 vd1185=vd1200|vd1199=vd1200|~rpoint(vd1200)|rR(vd1185,vd1199,vd1200)|rR(vd1199,vd1185,vd1200)|rR(vd1200,vd1199,vd1185)|~sQ382_spl),
% 2.28/0.75 inference(resolution,[status(thm)],[f3711,f142])).
% 2.28/0.75 fof(f3737,definition,(
% 2.28/0.75 sQ388_spl <=> (rR(vd1185,vd1199,vd1200))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f3738,plain,(
% 2.28/0.75 rR(vd1185,vd1199,vd1200)|~sQ388_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f3737])).
% 2.28/0.75 fof(f3740,definition,(
% 2.28/0.75 sQ389_spl <=> (rR(vd1199,vd1185,vd1200))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f3741,plain,(
% 2.28/0.75 rR(vd1199,vd1185,vd1200)|~sQ389_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f3740])).
% 2.28/0.75 fof(f3743,definition,(
% 2.28/0.75 sQ390_spl <=> (rR(vd1200,vd1199,vd1185))),
% 2.28/0.75 introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition])).
% 2.28/0.75 fof(f3744,plain,(
% 2.28/0.75 rR(vd1200,vd1199,vd1185)|~sQ390_spl),
% 2.28/0.75 inference(component_clause,[status(thm)],[f3743])).
% 2.28/0.75 fof(f3746,plain,(
% 2.28/0.75 sQ36_spl|sQ31_spl|~sQ14_spl|sQ388_spl|sQ389_spl|sQ390_spl|~sQ382_spl),
% 2.28/0.75 inference(split_clause,[status(thm)],[f3721,f1166,f1149,f1050,f3737,f3740,f3743,f3710])).
% 2.28/0.75 fof(f3754,plain,(
% 2.28/0.75 $false|~sQ390_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f3744,f942])).
% 2.28/0.75 fof(f3755,plain,(
% 2.28/0.75 ~sQ390_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f3754])).
% 2.28/0.75 fof(f3756,plain,(
% 2.28/0.75 $false|~sQ388_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f3738,f944])).
% 2.28/0.75 fof(f3757,plain,(
% 2.28/0.75 ~sQ388_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f3756])).
% 2.28/0.75 fof(f3758,plain,(
% 2.28/0.75 $false|~sQ389_spl),
% 2.28/0.75 inference(forward_subsumption_resolution,[status(thm)],[f3741,f945])).
% 2.28/0.75 fof(f3759,plain,(
% 2.28/0.75 ~sQ389_spl),
% 2.28/0.75 inference(contradiction_clause,[status(thm)],[f3758])).
% 2.28/0.75 fof(f3760,plain,(
% 2.28/0.75 $false),
% 2.28/0.75 inference(sat_refutation,[status(thm)],[f1071,f1085,f1087,f1089,f1195,f1242,f1369,f1569,f2033,f2720,f2817,f3713,f3746,f3755,f3757,f3759])).
% 2.28/0.75 % SZS output end CNFRefutation for theBenchmark.p
% 2.28/0.78 % Elapsed time: 0.406954 seconds
% 2.28/0.78 % CPU time: 2.803273 seconds
% 2.28/0.78 % Total memory used: 141.485 MB
% 2.28/0.78 % Net memory used: 137.819 MB
%------------------------------------------------------------------------------