%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO306+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 : n018.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 5.42s 1.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO306+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.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 15:20:27 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 5.42/1.18 % Refutation found
% 5.42/1.18 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.42/1.18 % SZS output start CNFRefutation for theBenchmark
% 5.42/1.18 fof(f1,conjecture,(
% 5.42/1.18 (? [Vd1306] :( vf(vd1287,vd1299) = vf(vd1287,Vd1306)& rR(Vd1306,vd1287,vd1302)& rpoint(Vd1306) ) )),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f2,negated_conjecture,(
% 5.42/1.18 ~((? [Vd1306] :( vf(vd1287,vd1299) = vf(vd1287,Vd1306)& rR(Vd1306,vd1287,vd1302)& rpoint(Vd1306) ) ))),
% 5.42/1.18 inference(negated_conjecture,[status(cth)],[f1])).
% 5.42/1.18 fof(f3,axiom,(
% 5.42/1.18 rless(vf(vd1287,vd1299),vf(vd1287,vd1302)) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f5,axiom,(
% 5.42/1.18 ron(vd1299,vd1295) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f6,axiom,(
% 5.42/1.18 ( vd1302 = vd1303& rR(vd1289,vd1287,vd1302)& rpoint(vd1303)& rR(vd1288,vd1287,vd1299) ) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f8,axiom,(
% 5.42/1.18 ron(vd1287,vd1297) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f9,axiom,(
% 5.42/1.18 rline(vd1297) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f10,axiom,(
% 5.42/1.18 ( 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) ) )) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f12,axiom,(
% 5.42/1.18 vd1299 = vd1300 ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f13,axiom,(
% 5.42/1.18 rpoint(vd1300) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f16,axiom,(
% 5.42/1.18 rline(vd1295) ),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f17,axiom,(
% 5.42/1.18 (! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :( ( rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111))& Vd1113 != Vd1115& Vd1109 != Vd1111& Vd1115 = Vd1116& rpoint(Vd1116)& Vd1113 = Vd1114& rpoint(Vd1114)& Vd1111 = Vd1112& rpoint(Vd1112)& Vd1109 = Vd1110& rpoint(Vd1110) )=> vf(Vd1109,vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116)) = vf(Vd1113,Vd1115) ) )),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f18,axiom,(
% 5.42/1.18 (! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :( ( rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111))& Vd1113 != Vd1115& Vd1109 != Vd1111& Vd1115 = Vd1116& rpoint(Vd1116)& Vd1113 = Vd1114& rpoint(Vd1114)& Vd1111 = Vd1112& rpoint(Vd1112)& Vd1109 = Vd1110& rpoint(Vd1110) )=> rR(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116),Vd1109,Vd1111) ) )),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f19,axiom,(
% 5.42/1.18 (! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :( ( rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111))& Vd1113 != Vd1115& Vd1109 != Vd1111& Vd1115 = Vd1116& rpoint(Vd1116)& Vd1113 = Vd1114& rpoint(Vd1114)& Vd1111 = Vd1112& rpoint(Vd1112)& Vd1109 = Vd1110& rpoint(Vd1110) )=> rpoint(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116)) ) )),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f49,axiom,(
% 5.42/1.18 (! [Vd340,Vd341,Vd342] :( ( rR(Vd341,Vd340,Vd342)& (? [Vd346] :( Vd342 = Vd346& rpoint(Vd346) ))& (? [Vd345] :( Vd341 = Vd345& rpoint(Vd345) ))& (? [Vd344] :( Vd340 = Vd344& rpoint(Vd344) ) ))=> ( ~ rR(Vd340,Vd341,Vd342)& Vd340 != Vd342& Vd340 != Vd341& rR(Vd341,Vd342,Vd340) ) ) )),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f76,axiom,(
% 5.42/1.18 (! [Vd408,Vd409,Vd410,Vd411] :( ( rR(Vd409,Vd408,Vd411)& rR(Vd409,Vd408,Vd410)& (? [Vd416] :( Vd411 = Vd416& rpoint(Vd416) ))& (? [Vd415] :( Vd410 = Vd415& rpoint(Vd415) ))& (? [Vd414] :( Vd409 = Vd414& rpoint(Vd414) ))& (? [Vd413] :( Vd408 = Vd413& rpoint(Vd413) ) ))=> ~ rR(Vd409,Vd410,Vd411) ) )),
% 5.42/1.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.42/1.18 fof(f129,plain,(
% 5.42/1.18 (![Vd1306]: ((~vf(vd1287,vd1299)=vf(vd1287,Vd1306)|~rR(Vd1306,vd1287,vd1302))|~rpoint(Vd1306)))),
% 5.42/1.18 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 5.42/1.18 fof(f130,plain,(
% 5.42/1.18 ![X0]: (~vf(vd1287,vd1299)=vf(vd1287,X0)|~rR(X0,vd1287,vd1302)|~rpoint(X0))),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f129])).
% 5.42/1.19 fof(f131,plain,(
% 5.42/1.19 rless(vf(vd1287,vd1299),vf(vd1287,vd1302))),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f3])).
% 5.42/1.19 fof(f133,plain,(
% 5.42/1.19 ron(vd1299,vd1295)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f5])).
% 5.42/1.19 fof(f134,plain,(
% 5.42/1.19 vd1302=vd1303),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f6])).
% 5.42/1.19 fof(f135,plain,(
% 5.42/1.19 rR(vd1289,vd1287,vd1302)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f6])).
% 5.42/1.19 fof(f136,plain,(
% 5.42/1.19 rpoint(vd1303)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f6])).
% 5.42/1.19 fof(f137,plain,(
% 5.42/1.19 rR(vd1288,vd1287,vd1299)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f6])).
% 5.42/1.19 fof(f139,plain,(
% 5.42/1.19 ron(vd1287,vd1297)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f8])).
% 5.42/1.19 fof(f140,plain,(
% 5.42/1.19 rline(vd1297)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f9])).
% 5.42/1.19 fof(f141,plain,(
% 5.42/1.19 (((((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))),
% 5.42/1.19 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)],[f10])).
% 5.42/1.19 fof(f144,plain,(
% 5.42/1.19 ~vd1287=vd1289),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f145,plain,(
% 5.42/1.19 ~vd1287=vd1288),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f146,plain,(
% 5.42/1.19 vd1289=sK0_skl),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f147,plain,(
% 5.42/1.19 rpoint(sK0_skl)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f148,plain,(
% 5.42/1.19 vd1288=sK1_skl),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f149,plain,(
% 5.42/1.19 rpoint(sK1_skl)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f150,plain,(
% 5.42/1.19 vd1287=sK2_skl),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f151,plain,(
% 5.42/1.19 rpoint(sK2_skl)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f141])).
% 5.42/1.19 fof(f155,plain,(
% 5.42/1.19 vd1299=vd1300),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f12])).
% 5.42/1.19 fof(f156,plain,(
% 5.42/1.19 rpoint(vd1300)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f13])).
% 5.42/1.19 fof(f159,plain,(
% 5.42/1.19 rline(vd1295)),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f16])).
% 5.42/1.19 fof(f160,plain,(
% 5.42/1.19 ![Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116]: (((((((((((~rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111))|Vd1113=Vd1115)|Vd1109=Vd1111)|~Vd1115=Vd1116)|~rpoint(Vd1116))|~Vd1113=Vd1114)|~rpoint(Vd1114))|~Vd1111=Vd1112)|~rpoint(Vd1112))|~Vd1109=Vd1110)|~rpoint(Vd1110))|vf(Vd1109,vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116))=vf(Vd1113,Vd1115))),
% 5.42/1.19 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 5.42/1.19 fof(f161,plain,(
% 5.42/1.19 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~rless(vf(X0,X1),vf(X2,X3))|X0=X1|X2=X3|~X1=X4|~rpoint(X4)|~X0=X5|~rpoint(X5)|~X3=X6|~rpoint(X6)|~X2=X7|~rpoint(X7)|vf(X2,vskolem1120(X2,X7,X3,X6,X0,X5,X1,X4))=vf(X0,X1))),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f160])).
% 5.42/1.19 fof(f162,plain,(
% 5.42/1.19 ![Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116]: (((((((((((~rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111))|Vd1113=Vd1115)|Vd1109=Vd1111)|~Vd1115=Vd1116)|~rpoint(Vd1116))|~Vd1113=Vd1114)|~rpoint(Vd1114))|~Vd1111=Vd1112)|~rpoint(Vd1112))|~Vd1109=Vd1110)|~rpoint(Vd1110))|rR(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116),Vd1109,Vd1111))),
% 5.42/1.19 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 5.42/1.19 fof(f163,plain,(
% 5.42/1.19 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~rless(vf(X0,X1),vf(X2,X3))|X0=X1|X2=X3|~X1=X4|~rpoint(X4)|~X0=X5|~rpoint(X5)|~X3=X6|~rpoint(X6)|~X2=X7|~rpoint(X7)|rR(vskolem1120(X2,X7,X3,X6,X0,X5,X1,X4),X2,X3))),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f162])).
% 5.42/1.19 fof(f164,plain,(
% 5.42/1.19 ![Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116]: (((((((((((~rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111))|Vd1113=Vd1115)|Vd1109=Vd1111)|~Vd1115=Vd1116)|~rpoint(Vd1116))|~Vd1113=Vd1114)|~rpoint(Vd1114))|~Vd1111=Vd1112)|~rpoint(Vd1112))|~Vd1109=Vd1110)|~rpoint(Vd1110))|rpoint(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116)))),
% 5.42/1.19 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 5.42/1.19 fof(f165,plain,(
% 5.42/1.19 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~rless(vf(X0,X1),vf(X2,X3))|X0=X1|X2=X3|~X1=X4|~rpoint(X4)|~X0=X5|~rpoint(X5)|~X3=X6|~rpoint(X6)|~X2=X7|~rpoint(X7)|rpoint(vskolem1120(X2,X7,X3,X6,X0,X5,X1,X4)))),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f164])).
% 5.42/1.19 fof(f268,plain,(
% 5.42/1.19 ![Vd340,Vd341,Vd342]: ((((~rR(Vd341,Vd340,Vd342)|(![Vd346]: (~Vd342=Vd346|~rpoint(Vd346))))|(![Vd345]: (~Vd341=Vd345|~rpoint(Vd345))))|(![Vd344]: (~Vd340=Vd344|~rpoint(Vd344))))|(((~rR(Vd340,Vd341,Vd342)&~Vd340=Vd342)&~Vd340=Vd341)&rR(Vd341,Vd342,Vd340)))),
% 5.42/1.19 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 5.42/1.19 fof(f272,plain,(
% 5.42/1.19 ![X0,X1,X2,X3,X4,X5]: (~rR(X0,X1,X2)|~X2=X3|~rpoint(X3)|~X0=X4|~rpoint(X4)|~X1=X5|~rpoint(X5)|rR(X0,X2,X1))),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f268])).
% 5.42/1.19 fof(f370,plain,(
% 5.42/1.19 ![Vd408,Vd409,Vd410,Vd411]: ((((((~rR(Vd409,Vd408,Vd411)|~rR(Vd409,Vd408,Vd410))|(![Vd416]: (~Vd411=Vd416|~rpoint(Vd416))))|(![Vd415]: (~Vd410=Vd415|~rpoint(Vd415))))|(![Vd414]: (~Vd409=Vd414|~rpoint(Vd414))))|(![Vd413]: (~Vd408=Vd413|~rpoint(Vd413))))|~rR(Vd409,Vd410,Vd411))),
% 5.42/1.19 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 5.42/1.19 fof(f371,plain,(
% 5.42/1.19 ![Vd409,Vd410,Vd411]: ((![Vd408]: (((((~rR(Vd409,Vd408,Vd411)|~rR(Vd409,Vd408,Vd410))|(![Vd416]: (~Vd411=Vd416|~rpoint(Vd416))))|(![Vd415]: (~Vd410=Vd415|~rpoint(Vd415))))|(![Vd414]: (~Vd409=Vd414|~rpoint(Vd414))))|(![Vd413]: (~Vd408=Vd413|~rpoint(Vd413)))))|~rR(Vd409,Vd410,Vd411))),
% 5.42/1.19 inference(miniscoping,[status(thm)],[f370])).
% 5.42/1.19 fof(f372,plain,(
% 5.42/1.19 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~rR(X0,X1,X2)|~rR(X0,X1,X3)|~X2=X4|~rpoint(X4)|~X3=X5|~rpoint(X5)|~X0=X6|~rpoint(X6)|~X1=X7|~rpoint(X7)|~rR(X0,X3,X2))),
% 5.42/1.19 inference(cnf_transformation,[status(thm)],[f371])).
% 5.42/1.19 fof(f707,plain,(
% 5.42/1.19 ![X0,X1,X2,X3]: (~rless(vf(X0,X1),vf(X2,X3))|X0=X1|X2=X3|~rpoint(X1)|~rpoint(X0)|~rpoint(X3)|~rpoint(X2)|vf(X2,vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1))=vf(X0,X1))),
% 5.42/1.19 inference(destructive_equality_resolution,[status(thm)],[f161])).
% 5.42/1.19 fof(f708,plain,(
% 5.42/1.19 ![X0,X1,X2,X3]: (~rless(vf(X0,X1),vf(X2,X3))|X0=X1|X2=X3|~rpoint(X1)|~rpoint(X0)|~rpoint(X3)|~rpoint(X2)|rR(vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1),X2,X3))),
% 5.42/1.19 inference(destructive_equality_resolution,[status(thm)],[f163])).
% 5.42/1.19 fof(f709,plain,(
% 5.42/1.19 ![X0,X1,X2,X3]: (~rless(vf(X0,X1),vf(X2,X3))|X0=X1|X2=X3|~rpoint(X1)|~rpoint(X0)|~rpoint(X3)|~rpoint(X2)|rpoint(vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1)))),
% 5.42/1.19 inference(destructive_equality_resolution,[status(thm)],[f165])).
% 5.42/1.19 fof(f765,plain,(
% 5.42/1.19 ![X0,X1,X2]: (~rR(X0,X1,X2)|~rpoint(X2)|~rpoint(X0)|~rpoint(X1)|rR(X0,X2,X1))),
% 5.42/1.19 inference(destructive_equality_resolution,[status(thm)],[f272])).
% 5.42/1.19 fof(f794,plain,(
% 5.42/1.19 ![X0,X1,X2,X3]: (~rR(X0,X1,X2)|~rR(X0,X1,X3)|~rpoint(X2)|~rpoint(X3)|~rpoint(X0)|~rpoint(X1)|~rR(X0,X3,X2))),
% 5.42/1.19 inference(destructive_equality_resolution,[status(thm)],[f372])).
% 5.42/1.19 fof(f943,definition,(
% 5.42/1.19 sQ9_spl <=> (rpoint(vd1289))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f945,plain,(
% 5.42/1.19 ~rpoint(vd1289)|sQ9_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f943])).
% 5.42/1.19 fof(f947,plain,(
% 5.42/1.19 rpoint(vd1302)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f134,f136])).
% 5.42/1.19 fof(f951,definition,(
% 5.42/1.19 sQ10_spl <=> (rpoint(vd1299))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f953,plain,(
% 5.42/1.19 ~rpoint(vd1299)|sQ10_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f951])).
% 5.42/1.19 fof(f954,definition,(
% 5.42/1.19 sQ11_spl <=> (rpoint(vd1288))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f956,plain,(
% 5.42/1.19 ~rpoint(vd1288)|sQ11_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f954])).
% 5.42/1.19 fof(f957,definition,(
% 5.42/1.19 sQ12_spl <=> (rpoint(vd1287))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f958,plain,(
% 5.42/1.19 rpoint(vd1287)|~sQ12_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f957])).
% 5.42/1.19 fof(f959,plain,(
% 5.42/1.19 ~rpoint(vd1287)|sQ12_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f957])).
% 5.42/1.19 fof(f964,definition,(
% 5.42/1.19 sQ14_spl <=> (rpoint(vd1302))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f966,plain,(
% 5.42/1.19 ~rpoint(vd1302)|sQ14_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f964])).
% 5.42/1.19 fof(f976,plain,(
% 5.42/1.19 ~rpoint(vd1302)|~rpoint(vd1289)|~rpoint(vd1287)|rR(vd1289,vd1302,vd1287)),
% 5.42/1.19 inference(resolution,[status(thm)],[f765,f135])).
% 5.42/1.19 fof(f981,definition,(
% 5.42/1.19 sQ17_spl <=> (rR(vd1289,vd1302,vd1287))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f982,plain,(
% 5.42/1.19 rR(vd1289,vd1302,vd1287)|~sQ17_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f981])).
% 5.42/1.19 fof(f984,plain,(
% 5.42/1.19 ~sQ14_spl|~sQ9_spl|~sQ12_spl|sQ17_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f976,f964,f943,f957,f981])).
% 5.42/1.19 fof(f986,plain,(
% 5.42/1.19 ![X0]: (~rR(vd1288,vd1287,X0)|~rpoint(vd1299)|~rpoint(X0)|~rpoint(vd1288)|~rpoint(vd1287)|~rR(vd1288,X0,vd1299))),
% 5.42/1.19 inference(resolution,[status(thm)],[f794,f137])).
% 5.42/1.19 fof(f987,plain,(
% 5.42/1.19 ![X0]: (~rR(vd1289,vd1287,X0)|~rpoint(vd1302)|~rpoint(X0)|~rpoint(vd1289)|~rpoint(vd1287)|~rR(vd1289,X0,vd1302))),
% 5.42/1.19 inference(resolution,[status(thm)],[f794,f135])).
% 5.42/1.19 fof(f988,definition,(
% 5.42/1.19 ![X0]: (sQ18_spl <=> (~rR(vd1288,vd1287,X0)|~rpoint(X0)|~rR(vd1288,X0,vd1299)))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f989,plain,(
% 5.42/1.19 ![X0]: (~rR(vd1288,vd1287,X0)|~rpoint(X0)|~rR(vd1288,X0,vd1299)|~sQ18_spl)),
% 5.42/1.19 inference(component_clause,[status(thm)],[f988])).
% 5.42/1.19 fof(f991,plain,(
% 5.42/1.19 sQ18_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f986,f988,f951,f954,f957])).
% 5.42/1.19 fof(f992,definition,(
% 5.42/1.19 ![X0]: (sQ19_spl <=> (~rR(vd1289,vd1287,X0)|~rpoint(X0)|~rR(vd1289,X0,vd1302)))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f993,plain,(
% 5.42/1.19 ![X0]: (~rR(vd1289,vd1287,X0)|~rpoint(X0)|~rR(vd1289,X0,vd1302)|~sQ19_spl)),
% 5.42/1.19 inference(component_clause,[status(thm)],[f992])).
% 5.42/1.19 fof(f995,plain,(
% 5.42/1.19 sQ19_spl|~sQ14_spl|~sQ9_spl|~sQ12_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f987,f992,f964,f943,f957])).
% 5.42/1.19 fof(f1006,plain,(
% 5.42/1.19 ~rpoint(sK0_skl)|sQ9_spl),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f146,f945])).
% 5.42/1.19 fof(f1009,plain,(
% 5.42/1.19 ~vd1287=sK0_skl),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f146,f144])).
% 5.42/1.19 fof(f1011,plain,(
% 5.42/1.19 rR(sK0_skl,vd1287,vd1302)),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f146,f135])).
% 5.42/1.19 fof(f1014,plain,(
% 5.42/1.19 ~vd1287=sK1_skl),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f148,f145])).
% 5.42/1.19 fof(f1015,plain,(
% 5.42/1.19 rR(sK1_skl,vd1287,vd1299)),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f148,f137])).
% 5.42/1.19 fof(f1018,plain,(
% 5.42/1.19 ~rpoint(sK2_skl)|sQ12_spl),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f150,f959])).
% 5.42/1.19 fof(f1019,plain,(
% 5.42/1.19 ron(sK2_skl,vd1297)),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f150,f139])).
% 5.42/1.19 fof(f1020,plain,(
% 5.42/1.19 rless(vf(vd1287,vd1299),vf(sK2_skl,vd1302))),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f150,f131])).
% 5.42/1.19 fof(f1021,plain,(
% 5.42/1.19 ![X0]: (~vf(vd1287,vd1299)=vf(vd1287,X0)|~rR(X0,sK2_skl,vd1302)|~rpoint(X0))),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f150,f130])).
% 5.42/1.19 fof(f1022,plain,(
% 5.42/1.19 rless(vf(sK2_skl,vd1299),vf(sK2_skl,vd1302))),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1020])).
% 5.42/1.19 fof(f1023,plain,(
% 5.42/1.19 ![X0]: (~vf(sK2_skl,vd1299)=vf(vd1287,X0)|~rR(X0,sK2_skl,vd1302)|~rpoint(X0))),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1021])).
% 5.42/1.19 fof(f1024,plain,(
% 5.42/1.19 ![X0]: (~vf(sK2_skl,vd1299)=vf(sK2_skl,X0)|~rR(X0,sK2_skl,vd1302)|~rpoint(X0))),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1023])).
% 5.42/1.19 fof(f1025,plain,(
% 5.42/1.19 $false|sQ9_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1006,f147])).
% 5.42/1.19 fof(f1026,plain,(
% 5.42/1.19 sQ9_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1025])).
% 5.42/1.19 fof(f1031,plain,(
% 5.42/1.19 rR(sK0_skl,sK2_skl,vd1302)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1011])).
% 5.42/1.19 fof(f1040,definition,(
% 5.42/1.19 sQ23_spl <=> (rpoint(sK0_skl))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1042,plain,(
% 5.42/1.19 ~rpoint(sK0_skl)|sQ23_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1040])).
% 5.42/1.19 fof(f1047,definition,(
% 5.42/1.19 sQ25_spl <=> (rpoint(sK2_skl))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1049,plain,(
% 5.42/1.19 ~rpoint(sK2_skl)|sQ25_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1047])).
% 5.42/1.19 fof(f1063,plain,(
% 5.42/1.19 $false|sQ14_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f966,f947])).
% 5.42/1.19 fof(f1064,plain,(
% 5.42/1.19 sQ14_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1063])).
% 5.42/1.19 fof(f1065,plain,(
% 5.42/1.19 $false|sQ23_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1042,f147])).
% 5.42/1.19 fof(f1066,plain,(
% 5.42/1.19 sQ23_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1065])).
% 5.42/1.19 fof(f1077,definition,(
% 5.42/1.19 sQ31_spl <=> (rline(vd1295))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1079,plain,(
% 5.42/1.19 ~rline(vd1295)|sQ31_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1077])).
% 5.42/1.19 fof(f1084,definition,(
% 5.42/1.19 sQ33_spl <=> (rline(vd1297))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1086,plain,(
% 5.42/1.19 ~rline(vd1297)|sQ33_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1084])).
% 5.42/1.19 fof(f1088,plain,(
% 5.42/1.19 $false|sQ12_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f151,f1018])).
% 5.42/1.19 fof(f1089,plain,(
% 5.42/1.19 sQ12_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1088])).
% 5.42/1.19 fof(f1092,plain,(
% 5.42/1.19 rR(sK0_skl,vd1302,vd1287)|~sQ17_spl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f146,f982])).
% 5.42/1.19 fof(f1093,plain,(
% 5.42/1.19 rR(sK0_skl,vd1302,sK2_skl)|~sQ17_spl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1092])).
% 5.42/1.19 fof(f1094,plain,(
% 5.42/1.19 ![X0]: (~rR(sK0_skl,vd1287,X0)|~rpoint(X0)|~rR(vd1289,X0,vd1302)|~sQ19_spl)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f146,f993])).
% 5.42/1.19 fof(f1095,plain,(
% 5.42/1.19 ![X0]: (~rR(sK0_skl,sK2_skl,X0)|~rpoint(X0)|~rR(vd1289,X0,vd1302)|~sQ19_spl)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1094])).
% 5.42/1.19 fof(f1096,plain,(
% 5.42/1.19 ![X0]: (~rR(sK0_skl,sK2_skl,X0)|~rpoint(X0)|~rR(sK0_skl,X0,vd1302)|~sQ19_spl)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f146,f1095])).
% 5.42/1.19 fof(f1100,plain,(
% 5.42/1.19 rpoint(sK2_skl)|~sQ12_spl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f958])).
% 5.42/1.19 fof(f1101,plain,(
% 5.42/1.19 rpoint(vd1299)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f155,f156])).
% 5.42/1.19 fof(f1109,definition,(
% 5.42/1.19 sQ35_spl <=> (rpoint(sK1_skl))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1111,plain,(
% 5.42/1.19 ~rpoint(sK1_skl)|sQ35_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1109])).
% 5.42/1.19 fof(f1113,plain,(
% 5.42/1.19 ~rpoint(sK1_skl)|sQ11_spl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f148,f956])).
% 5.42/1.19 fof(f1114,plain,(
% 5.42/1.19 $false|sQ11_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1113,f149])).
% 5.42/1.19 fof(f1115,plain,(
% 5.42/1.19 sQ11_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1114])).
% 5.42/1.19 fof(f1123,plain,(
% 5.42/1.19 $false|sQ10_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f953,f1101])).
% 5.42/1.19 fof(f1124,plain,(
% 5.42/1.19 sQ10_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1123])).
% 5.42/1.19 fof(f1129,plain,(
% 5.42/1.19 ![X0]: (~rR(sK1_skl,vd1287,X0)|~rpoint(X0)|~rR(vd1288,X0,vd1299)|~sQ18_spl)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f148,f989])).
% 5.42/1.19 fof(f1130,plain,(
% 5.42/1.19 ![X0]: (~rR(sK1_skl,sK2_skl,X0)|~rpoint(X0)|~rR(vd1288,X0,vd1299)|~sQ18_spl)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1129])).
% 5.42/1.19 fof(f1131,plain,(
% 5.42/1.19 ![X0]: (~rR(sK1_skl,sK2_skl,X0)|~rpoint(X0)|~rR(sK1_skl,X0,vd1299)|~sQ18_spl)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f148,f1130])).
% 5.42/1.19 fof(f1178,plain,(
% 5.42/1.19 $false|sQ25_spl|~sQ12_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1100,f1049])).
% 5.42/1.19 fof(f1179,plain,(
% 5.42/1.19 sQ25_spl|~sQ12_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1178])).
% 5.42/1.19 fof(f1200,plain,(
% 5.42/1.19 $false|sQ31_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1079,f159])).
% 5.42/1.19 fof(f1201,plain,(
% 5.42/1.19 sQ31_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1200])).
% 5.42/1.19 fof(f1202,plain,(
% 5.42/1.19 $false|sQ35_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1111,f149])).
% 5.42/1.19 fof(f1203,plain,(
% 5.42/1.19 sQ35_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1202])).
% 5.42/1.19 fof(f1204,plain,(
% 5.42/1.19 rR(sK1_skl,sK2_skl,vd1299)),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1015])).
% 5.42/1.19 fof(f1230,plain,(
% 5.42/1.19 sK2_skl=vd1299|sK2_skl=vd1302|~rpoint(vd1299)|~rpoint(sK2_skl)|~rpoint(vd1302)|~rpoint(sK2_skl)|rpoint(vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299))),
% 5.42/1.19 inference(resolution,[status(thm)],[f1022,f709])).
% 5.42/1.19 fof(f1231,plain,(
% 5.42/1.19 sK2_skl=vd1299|sK2_skl=vd1302|~rpoint(vd1299)|~rpoint(sK2_skl)|~rpoint(vd1302)|~rpoint(sK2_skl)|rR(vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299),sK2_skl,vd1302)),
% 5.42/1.19 inference(resolution,[status(thm)],[f1022,f708])).
% 5.42/1.19 fof(f1232,plain,(
% 5.42/1.19 sK2_skl=vd1299|sK2_skl=vd1302|~rpoint(vd1299)|~rpoint(sK2_skl)|~rpoint(vd1302)|~rpoint(sK2_skl)|vf(sK2_skl,vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299))=vf(sK2_skl,vd1299)),
% 5.42/1.19 inference(resolution,[status(thm)],[f1022,f707])).
% 5.42/1.19 fof(f1233,definition,(
% 5.42/1.19 sQ54_spl <=> (sK2_skl=vd1299)),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1234,plain,(
% 5.42/1.19 sK2_skl=vd1299|~sQ54_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1233])).
% 5.42/1.19 fof(f1236,definition,(
% 5.42/1.19 sQ55_spl <=> (sK2_skl=vd1302)),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1237,plain,(
% 5.42/1.19 sK2_skl=vd1302|~sQ55_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1236])).
% 5.42/1.19 fof(f1239,definition,(
% 5.42/1.19 sQ56_spl <=> (rpoint(vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299)))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1242,plain,(
% 5.42/1.19 sQ54_spl|sQ55_spl|~sQ10_spl|~sQ25_spl|~sQ14_spl|sQ56_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f1230,f1233,f1236,f951,f1047,f964,f1239])).
% 5.42/1.19 fof(f1243,definition,(
% 5.42/1.19 sQ57_spl <=> (rR(vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299),sK2_skl,vd1302))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1244,plain,(
% 5.42/1.19 rR(vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299),sK2_skl,vd1302)|~sQ57_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1243])).
% 5.42/1.19 fof(f1246,plain,(
% 5.42/1.19 sQ54_spl|sQ55_spl|~sQ10_spl|~sQ25_spl|~sQ14_spl|sQ57_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f1231,f1233,f1236,f951,f1047,f964,f1243])).
% 5.42/1.19 fof(f1247,definition,(
% 5.42/1.19 sQ58_spl <=> (vf(sK2_skl,vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299))=vf(sK2_skl,vd1299))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1250,plain,(
% 5.42/1.19 sQ54_spl|sQ55_spl|~sQ10_spl|~sQ25_spl|~sQ14_spl|sQ58_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f1232,f1233,f1236,f951,f1047,f964,f1247])).
% 5.42/1.19 fof(f1251,plain,(
% 5.42/1.19 $false|sQ33_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f140,f1086])).
% 5.42/1.19 fof(f1252,plain,(
% 5.42/1.19 sQ33_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1251])).
% 5.42/1.19 fof(f1253,plain,(
% 5.42/1.19 ~sK2_skl=sK0_skl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1009])).
% 5.42/1.19 fof(f1282,plain,(
% 5.42/1.19 rR(sK0_skl,sK2_skl,sK2_skl)|~sQ55_spl),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f1237,f1031])).
% 5.42/1.19 fof(f1313,plain,(
% 5.42/1.19 ~sK2_skl=sK1_skl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f150,f1014])).
% 5.42/1.19 fof(f1343,plain,(
% 5.42/1.19 rR(sK1_skl,sK2_skl,sK2_skl)|~sQ54_spl),
% 5.42/1.19 inference(backward_demodulation,[status(thm)],[f1234,f1204])).
% 5.42/1.19 fof(f1472,plain,(
% 5.42/1.19 ~rpoint(sK2_skl)|~rpoint(sK0_skl)|~rpoint(vd1302)|rR(sK0_skl,sK2_skl,vd1302)|~sQ17_spl),
% 5.42/1.19 inference(resolution,[status(thm)],[f1093,f765])).
% 5.42/1.19 fof(f1486,definition,(
% 5.42/1.19 sQ75_spl <=> (rR(sK0_skl,sK2_skl,vd1302))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1489,plain,(
% 5.42/1.19 ~sQ25_spl|~sQ23_spl|~sQ14_spl|sQ75_spl|~sQ17_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f1472,f1047,f1040,f964,f1486,f981])).
% 5.42/1.19 fof(f1564,plain,(
% 5.42/1.19 ~rpoint(vd1299)|~rR(sK1_skl,vd1299,vd1299)|~sQ18_spl),
% 5.42/1.19 inference(resolution,[status(thm)],[f1131,f1204])).
% 5.42/1.19 fof(f1565,definition,(
% 5.42/1.19 sQ83_spl <=> (rR(sK1_skl,vd1299,vd1299))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1567,plain,(
% 5.42/1.19 ~rR(sK1_skl,vd1299,vd1299)|sQ83_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1565])).
% 5.42/1.19 fof(f1568,plain,(
% 5.42/1.19 ~sQ10_spl|~sQ83_spl|~sQ18_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f1564,f951,f1565,f988])).
% 5.42/1.19 fof(f1763,definition,(
% 5.42/1.19 sQ120_spl <=> (ron(vd1299,vd1295))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1765,plain,(
% 5.42/1.19 ~ron(vd1299,vd1295)|sQ120_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1763])).
% 5.42/1.19 fof(f1777,plain,(
% 5.42/1.19 $false|sQ120_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1765,f133])).
% 5.42/1.19 fof(f1778,plain,(
% 5.42/1.19 sQ120_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1777])).
% 5.42/1.19 fof(f1809,definition,(
% 5.42/1.19 sQ130_spl <=> (sK1_skl=sK2_skl)),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f1810,plain,(
% 5.42/1.19 sK1_skl=sK2_skl|~sQ130_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f1809])).
% 5.42/1.19 fof(f1906,plain,(
% 5.42/1.19 ~rR(sK1_skl,sK2_skl,vd1299)|~sQ54_spl|sQ83_spl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f1234,f1567])).
% 5.42/1.19 fof(f1907,plain,(
% 5.42/1.19 ~rR(sK1_skl,sK2_skl,sK2_skl)|~sQ54_spl|sQ83_spl),
% 5.42/1.19 inference(forward_demodulation,[status(thm)],[f1234,f1906])).
% 5.42/1.19 fof(f1908,plain,(
% 5.42/1.19 $false|sQ83_spl|~sQ54_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1343,f1907])).
% 5.42/1.19 fof(f1909,plain,(
% 5.42/1.19 sQ83_spl|~sQ54_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f1908])).
% 5.42/1.19 fof(f2347,plain,(
% 5.42/1.19 $false|~sQ130_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f1810,f1313])).
% 5.42/1.19 fof(f2348,plain,(
% 5.42/1.19 ~sQ130_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f2347])).
% 5.42/1.19 fof(f2409,definition,(
% 5.42/1.19 sQ192_spl <=> (ron(sK2_skl,vd1297))),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f2411,plain,(
% 5.42/1.19 ~ron(sK2_skl,vd1297)|sQ192_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f2409])).
% 5.42/1.19 fof(f2416,plain,(
% 5.42/1.19 $false|sQ192_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f2411,f1019])).
% 5.42/1.19 fof(f2417,plain,(
% 5.42/1.19 sQ192_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f2416])).
% 5.42/1.19 fof(f2808,definition,(
% 5.42/1.19 sQ228_spl <=> (sK2_skl=sK0_skl)),
% 5.42/1.19 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 5.42/1.19 fof(f2809,plain,(
% 5.42/1.19 sK2_skl=sK0_skl|~sQ228_spl),
% 5.42/1.19 inference(component_clause,[status(thm)],[f2808])).
% 5.42/1.19 fof(f3043,plain,(
% 5.42/1.19 $false|~sQ228_spl),
% 5.42/1.19 inference(forward_subsumption_resolution,[status(thm)],[f2809,f1253])).
% 5.42/1.19 fof(f3044,plain,(
% 5.42/1.19 ~sQ228_spl),
% 5.42/1.19 inference(contradiction_clause,[status(thm)],[f3043])).
% 5.42/1.19 fof(f3824,plain,(
% 5.42/1.19 ~vf(sK2_skl,vd1299)=vf(sK2_skl,vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299))|~rpoint(vskolem1120(sK2_skl,sK2_skl,vd1302,vd1302,sK2_skl,sK2_skl,vd1299,vd1299))|~sQ57_spl),
% 5.42/1.19 inference(resolution,[status(thm)],[f1244,f1024])).
% 5.42/1.19 fof(f3833,plain,(
% 5.42/1.19 ~sQ58_spl|~sQ56_spl|~sQ57_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f3824,f1247,f1239,f1243])).
% 5.42/1.19 fof(f3870,plain,(
% 5.42/1.19 ~rpoint(sK2_skl)|~rR(sK0_skl,sK2_skl,vd1302)|~sQ55_spl|~sQ19_spl),
% 5.42/1.19 inference(resolution,[status(thm)],[f1282,f1096])).
% 5.42/1.19 fof(f3882,plain,(
% 5.42/1.19 ~sQ25_spl|~sQ75_spl|~sQ55_spl|~sQ19_spl),
% 5.42/1.19 inference(split_clause,[status(thm)],[f3870,f1047,f1486,f1236,f992])).
% 5.42/1.19 fof(f3915,plain,(
% 5.42/1.19 $false),
% 5.42/1.19 inference(sat_refutation,[status(thm)],[f984,f991,f995,f1026,f1064,f1066,f1089,f1115,f1124,f1179,f1201,f1203,f1242,f1246,f1250,f1252,f1489,f1568,f1778,f1909,f2348,f2417,f3044,f3833,f3882])).
% 5.42/1.19 % SZS output end CNFRefutation for theBenchmark.p
% 5.42/1.21 % Elapsed time: 0.828752 seconds
% 5.42/1.21 % CPU time: 6.141091 seconds
% 5.42/1.21 % Total memory used: 159.484 MB
% 5.42/1.21 % Net memory used: 152.891 MB
%------------------------------------------------------------------------------