%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO332+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 : n005.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:22 PM UTC 2026
% Result : Theorem 0.12s 0.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO332+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.08/0.56 % Computer : n005.cluster.edu
% 0.08/0.56 % Model : x86_64 x86_64
% 0.08/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.56 % Memory : 8046.5625MB
% 0.08/0.56 % OS : Linux 6.8.0-71-generic
% 0.08/0.56 % CPULimit : 300
% 0.08/0.56 % WCLimit : 300
% 0.08/0.56 % DateTime : Sun Sep 20 15:24:18 UTC 2026
% 0.08/0.57 % CPUTime :
% 0.08/0.60 % Drodi V4.1.1
% 0.12/0.90 % Refutation found
% 0.12/0.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.90 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.90 fof(f1,conjecture,(
% 0.12/0.90 (? [Vd1371] :( vf(vd1362,Vd1371) = vf(vd1361,vd1363)& rR(Vd1371,vd1362,vd1361)& rpoint(Vd1371) ) )),
% 0.12/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.90 fof(f2,negated_conjecture,(
% 0.12/0.90 ~((? [Vd1371] :( vf(vd1362,Vd1371) = vf(vd1361,vd1363)& rR(Vd1371,vd1362,vd1361)& rpoint(Vd1371) ) ))),
% 0.12/0.90 inference(negated_conjecture,[status(cth)],[f1])).
% 0.12/0.90 fof(f3,axiom,(
% 0.12/0.90 rless(vf(vd1361,vd1363),vf(vd1361,vd1362)) ),
% 0.12/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.90 fof(f7,axiom,(
% 0.12/0.90 vd1361 != vd1363 ),
% 0.12/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.90 fof(f8,axiom,(
% 0.12/0.90 vd1361 != vd1362 ),
% 0.12/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.90 fof(f9,axiom,(
% 0.12/0.90 (? [Vd1368] :( vd1363 = Vd1368& rpoint(Vd1368) ) )),
% 0.12/0.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.90 fof(f10,axiom,(
% 0.12/0.90 (? [Vd1367] :( vd1362 = Vd1367& rpoint(Vd1367) ) )),
% 0.12/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.91 fof(f11,axiom,(
% 0.12/0.91 (? [Vd1366] :( vd1361 = Vd1366& rpoint(Vd1366) ) )),
% 0.12/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.91 fof(f17,axiom,(
% 0.12/0.91 (! [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) ) )),
% 0.12/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.91 fof(f18,axiom,(
% 0.12/0.91 (! [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) ) )),
% 0.12/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.91 fof(f19,axiom,(
% 0.12/0.91 (! [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)) ) )),
% 0.12/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.91 fof(f26,axiom,(
% 0.12/0.91 (! [Vd761,Vd762] :( ( (? [Vd765] :( Vd762 = Vd765& rpoint(Vd765) ))& (? [Vd764] :( Vd761 = Vd764& rpoint(Vd764) ) ))=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ) )),
% 0.12/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.91 fof(f127,plain,(
% 0.12/0.91 (![Vd1371]: ((~vf(vd1362,Vd1371)=vf(vd1361,vd1363)|~rR(Vd1371,vd1362,vd1361))|~rpoint(Vd1371)))),
% 0.12/0.91 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.91 fof(f128,plain,(
% 0.12/0.91 ![X0]: (~vf(vd1362,X0)=vf(vd1361,vd1363)|~rR(X0,vd1362,vd1361)|~rpoint(X0))),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f127])).
% 0.12/0.91 fof(f129,plain,(
% 0.12/0.91 rless(vf(vd1361,vd1363),vf(vd1361,vd1362))),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.91 fof(f133,plain,(
% 0.12/0.91 ~vd1361=vd1363),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.91 fof(f134,plain,(
% 0.12/0.91 ~vd1361=vd1362),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.91 fof(f135,plain,(
% 0.12/0.91 (vd1363=sK0_skl&rpoint(sK0_skl))),
% 0.12/0.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1368,sK0_skl)],[f9])).
% 0.12/0.91 fof(f136,plain,(
% 0.12/0.91 vd1363=sK0_skl),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f135])).
% 0.12/0.91 fof(f137,plain,(
% 0.12/0.91 rpoint(sK0_skl)),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f135])).
% 0.12/0.91 fof(f138,plain,(
% 0.12/0.91 (vd1362=sK1_skl&rpoint(sK1_skl))),
% 0.12/0.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd1367,sK1_skl)],[f10])).
% 0.12/0.91 fof(f139,plain,(
% 0.12/0.91 vd1362=sK1_skl),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f138])).
% 0.12/0.91 fof(f140,plain,(
% 0.12/0.91 rpoint(sK1_skl)),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f138])).
% 0.12/0.91 fof(f141,plain,(
% 0.12/0.91 (vd1361=sK2_skl&rpoint(sK2_skl))),
% 0.12/0.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd1366,sK2_skl)],[f11])).
% 0.12/0.91 fof(f142,plain,(
% 0.12/0.91 vd1361=sK2_skl),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f141])).
% 0.12/0.91 fof(f143,plain,(
% 0.12/0.91 rpoint(sK2_skl)),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f141])).
% 0.12/0.91 fof(f169,plain,(
% 0.12/0.91 ![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))),
% 0.12/0.91 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.12/0.91 fof(f170,plain,(
% 0.12/0.91 ![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))),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f169])).
% 0.12/0.91 fof(f171,plain,(
% 0.12/0.91 ![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))),
% 0.12/0.91 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.12/0.91 fof(f172,plain,(
% 0.12/0.91 ![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))),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f171])).
% 0.12/0.91 fof(f173,plain,(
% 0.12/0.91 ![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)))),
% 0.12/0.91 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.12/0.91 fof(f174,plain,(
% 0.12/0.91 ![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)))),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f173])).
% 0.12/0.91 fof(f199,plain,(
% 0.12/0.91 ![Vd761,Vd762]: (((![Vd765]: (~Vd762=Vd765|~rpoint(Vd765)))|(![Vd764]: (~Vd761=Vd764|~rpoint(Vd764))))|vf(Vd761,Vd762)=vf(Vd762,Vd761))),
% 0.12/0.91 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.12/0.91 fof(f200,plain,(
% 0.12/0.91 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=vf(X0,X2))),
% 0.12/0.91 inference(cnf_transformation,[status(thm)],[f199])).
% 0.12/0.91 fof(f713,plain,(
% 0.12/0.91 ![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))),
% 0.12/0.91 inference(destructive_equality_resolution,[status(thm)],[f170])).
% 0.12/0.91 fof(f714,plain,(
% 0.12/0.91 ![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))),
% 0.12/0.91 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 0.12/0.91 fof(f715,plain,(
% 0.12/0.91 ![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)))),
% 0.12/0.91 inference(destructive_equality_resolution,[status(thm)],[f174])).
% 0.12/0.91 fof(f728,plain,(
% 0.12/0.91 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|vf(X1,X0)=vf(X0,X1))),
% 0.12/0.91 inference(destructive_equality_resolution,[status(thm)],[f200])).
% 0.12/0.91 fof(f936,plain,(
% 0.12/0.91 ~vd1361=sK0_skl),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f136,f133])).
% 0.12/0.91 fof(f938,plain,(
% 0.12/0.91 rless(vf(vd1361,sK0_skl),vf(vd1361,vd1362))),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f136,f129])).
% 0.12/0.91 fof(f939,plain,(
% 0.12/0.91 ![X0]: (~vf(vd1362,X0)=vf(vd1361,sK0_skl)|~rR(X0,vd1362,vd1361)|~rpoint(X0))),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f136,f128])).
% 0.12/0.91 fof(f941,plain,(
% 0.12/0.91 ~vd1361=sK1_skl),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f139,f134])).
% 0.12/0.91 fof(f942,plain,(
% 0.12/0.91 ![X0]: (~vf(sK1_skl,X0)=vf(vd1361,sK0_skl)|~rR(X0,vd1362,vd1361)|~rpoint(X0))),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f139,f939])).
% 0.12/0.91 fof(f943,plain,(
% 0.12/0.91 ![X0]: (~vf(sK1_skl,X0)=vf(vd1361,sK0_skl)|~rR(X0,sK1_skl,vd1361)|~rpoint(X0))),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f139,f942])).
% 0.12/0.91 fof(f945,plain,(
% 0.12/0.91 ![X0]: (~rpoint(X0)|vf(X0,sK0_skl)=vf(sK0_skl,X0))),
% 0.12/0.91 inference(resolution,[status(thm)],[f728,f137])).
% 0.12/0.91 fof(f946,plain,(
% 0.12/0.91 ![X0]: (~rpoint(X0)|vf(X0,sK1_skl)=vf(sK1_skl,X0))),
% 0.12/0.91 inference(resolution,[status(thm)],[f140,f728])).
% 0.12/0.91 fof(f947,plain,(
% 0.12/0.91 ~sK2_skl=sK0_skl),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f142,f936])).
% 0.12/0.91 fof(f948,plain,(
% 0.12/0.91 ![X0]: (~vf(sK1_skl,X0)=vf(vd1361,sK0_skl)|~rR(X0,sK1_skl,sK2_skl)|~rpoint(X0))),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f142,f943])).
% 0.12/0.91 fof(f949,plain,(
% 0.12/0.91 ![X0]: (~vf(sK1_skl,X0)=vf(sK2_skl,sK0_skl)|~rR(X0,sK1_skl,sK2_skl)|~rpoint(X0))),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f142,f948])).
% 0.12/0.91 fof(f960,plain,(
% 0.12/0.91 ~sK2_skl=sK1_skl),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f142,f941])).
% 0.12/0.91 fof(f1000,plain,(
% 0.12/0.91 vf(sK2_skl,sK0_skl)=vf(sK0_skl,sK2_skl)),
% 0.12/0.91 inference(resolution,[status(thm)],[f945,f143])).
% 0.12/0.91 fof(f1004,plain,(
% 0.12/0.91 ![X0]: (~vf(sK1_skl,X0)=vf(sK0_skl,sK2_skl)|~rR(X0,sK1_skl,sK2_skl)|~rpoint(X0))),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f1000,f949])).
% 0.12/0.91 fof(f1022,plain,(
% 0.12/0.91 rless(vf(sK2_skl,sK0_skl),vf(vd1361,vd1362))),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f142,f938])).
% 0.12/0.91 fof(f1023,plain,(
% 0.12/0.91 rless(vf(sK0_skl,sK2_skl),vf(vd1361,vd1362))),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f1000,f1022])).
% 0.12/0.91 fof(f1024,plain,(
% 0.12/0.91 rless(vf(sK0_skl,sK2_skl),vf(sK2_skl,vd1362))),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f142,f1023])).
% 0.12/0.91 fof(f1025,plain,(
% 0.12/0.91 rless(vf(sK0_skl,sK2_skl),vf(sK2_skl,sK1_skl))),
% 0.12/0.91 inference(forward_demodulation,[status(thm)],[f139,f1024])).
% 0.12/0.91 fof(f1027,plain,(
% 0.12/0.91 vf(sK2_skl,sK1_skl)=vf(sK1_skl,sK2_skl)),
% 0.12/0.91 inference(resolution,[status(thm)],[f946,f143])).
% 0.12/0.91 fof(f1037,definition,(
% 0.12/0.91 sQ8_spl <=> (sK0_skl=sK2_skl)),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1038,plain,(
% 0.12/0.91 sK0_skl=sK2_skl|~sQ8_spl),
% 0.12/0.91 inference(component_clause,[status(thm)],[f1037])).
% 0.12/0.91 fof(f1040,definition,(
% 0.12/0.91 sQ9_spl <=> (sK2_skl=sK1_skl)),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1041,plain,(
% 0.12/0.91 sK2_skl=sK1_skl|~sQ9_spl),
% 0.12/0.91 inference(component_clause,[status(thm)],[f1040])).
% 0.12/0.91 fof(f1043,definition,(
% 0.12/0.91 sQ10_spl <=> (rpoint(sK2_skl))),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1045,plain,(
% 0.12/0.91 ~rpoint(sK2_skl)|sQ10_spl),
% 0.12/0.91 inference(component_clause,[status(thm)],[f1043])).
% 0.12/0.91 fof(f1046,definition,(
% 0.12/0.91 sQ11_spl <=> (rpoint(sK0_skl))),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1048,plain,(
% 0.12/0.91 ~rpoint(sK0_skl)|sQ11_spl),
% 0.12/0.91 inference(component_clause,[status(thm)],[f1046])).
% 0.12/0.91 fof(f1049,definition,(
% 0.12/0.91 sQ12_spl <=> (rpoint(sK1_skl))),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1051,plain,(
% 0.12/0.91 ~rpoint(sK1_skl)|sQ12_spl),
% 0.12/0.91 inference(component_clause,[status(thm)],[f1049])).
% 0.12/0.91 fof(f1089,plain,(
% 0.12/0.91 $false|sQ11_spl),
% 0.12/0.91 inference(forward_subsumption_resolution,[status(thm)],[f1048,f137])).
% 0.12/0.91 fof(f1090,plain,(
% 0.12/0.91 sQ11_spl),
% 0.12/0.91 inference(contradiction_clause,[status(thm)],[f1089])).
% 0.12/0.91 fof(f1091,plain,(
% 0.12/0.91 $false|sQ10_spl),
% 0.12/0.91 inference(forward_subsumption_resolution,[status(thm)],[f1045,f143])).
% 0.12/0.91 fof(f1092,plain,(
% 0.12/0.91 sQ10_spl),
% 0.12/0.91 inference(contradiction_clause,[status(thm)],[f1091])).
% 0.12/0.91 fof(f1093,plain,(
% 0.12/0.91 $false|~sQ8_spl),
% 0.12/0.91 inference(forward_subsumption_resolution,[status(thm)],[f1038,f947])).
% 0.12/0.91 fof(f1094,plain,(
% 0.12/0.91 ~sQ8_spl),
% 0.12/0.91 inference(contradiction_clause,[status(thm)],[f1093])).
% 0.12/0.91 fof(f1095,plain,(
% 0.12/0.91 $false|sQ12_spl),
% 0.12/0.91 inference(forward_subsumption_resolution,[status(thm)],[f1051,f140])).
% 0.12/0.91 fof(f1096,plain,(
% 0.12/0.91 sQ12_spl),
% 0.12/0.91 inference(contradiction_clause,[status(thm)],[f1095])).
% 0.12/0.91 fof(f1102,plain,(
% 0.12/0.91 $false|~sQ9_spl),
% 0.12/0.91 inference(forward_subsumption_resolution,[status(thm)],[f1041,f960])).
% 0.12/0.91 fof(f1103,plain,(
% 0.12/0.91 ~sQ9_spl),
% 0.12/0.91 inference(contradiction_clause,[status(thm)],[f1102])).
% 0.12/0.91 fof(f1184,plain,(
% 0.12/0.91 rless(vf(sK0_skl,sK2_skl),vf(sK1_skl,sK2_skl))),
% 0.12/0.91 inference(backward_demodulation,[status(thm)],[f1027,f1025])).
% 0.12/0.91 fof(f1217,plain,(
% 0.12/0.91 sK0_skl=sK2_skl|sK1_skl=sK2_skl|~rpoint(sK2_skl)|~rpoint(sK0_skl)|~rpoint(sK2_skl)|~rpoint(sK1_skl)|rpoint(vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl))),
% 0.12/0.91 inference(resolution,[status(thm)],[f1184,f715])).
% 0.12/0.91 fof(f1218,plain,(
% 0.12/0.91 sK0_skl=sK2_skl|sK1_skl=sK2_skl|~rpoint(sK2_skl)|~rpoint(sK0_skl)|~rpoint(sK2_skl)|~rpoint(sK1_skl)|rR(vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl),sK1_skl,sK2_skl)),
% 0.12/0.91 inference(resolution,[status(thm)],[f1184,f714])).
% 0.12/0.91 fof(f1219,plain,(
% 0.12/0.91 sK0_skl=sK2_skl|sK1_skl=sK2_skl|~rpoint(sK2_skl)|~rpoint(sK0_skl)|~rpoint(sK2_skl)|~rpoint(sK1_skl)|vf(sK1_skl,vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl))=vf(sK0_skl,sK2_skl)),
% 0.12/0.91 inference(resolution,[status(thm)],[f1184,f713])).
% 0.12/0.91 fof(f1220,definition,(
% 0.12/0.91 sQ43_spl <=> (rpoint(vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl)))),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1223,plain,(
% 0.12/0.91 sQ8_spl|sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ43_spl),
% 0.12/0.91 inference(split_clause,[status(thm)],[f1217,f1037,f1040,f1043,f1046,f1049,f1220])).
% 0.12/0.91 fof(f1224,definition,(
% 0.12/0.91 sQ44_spl <=> (rR(vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl),sK1_skl,sK2_skl))),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1225,plain,(
% 0.12/0.91 rR(vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl),sK1_skl,sK2_skl)|~sQ44_spl),
% 0.12/0.91 inference(component_clause,[status(thm)],[f1224])).
% 0.12/0.91 fof(f1227,plain,(
% 0.12/0.91 sQ8_spl|sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ44_spl),
% 0.12/0.91 inference(split_clause,[status(thm)],[f1218,f1037,f1040,f1043,f1046,f1049,f1224])).
% 0.12/0.91 fof(f1228,definition,(
% 0.12/0.91 sQ45_spl <=> (vf(sK1_skl,vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl))=vf(sK0_skl,sK2_skl))),
% 0.12/0.91 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.91 fof(f1231,plain,(
% 0.12/0.91 sQ8_spl|sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ45_spl),
% 0.12/0.91 inference(split_clause,[status(thm)],[f1219,f1037,f1040,f1043,f1046,f1049,f1228])).
% 0.12/0.91 fof(f1336,plain,(
% 0.12/0.91 ~vf(sK1_skl,vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl))=vf(sK0_skl,sK2_skl)|~rpoint(vskolem1120(sK1_skl,sK1_skl,sK2_skl,sK2_skl,sK0_skl,sK0_skl,sK2_skl,sK2_skl))|~sQ44_spl),
% 0.12/0.91 inference(resolution,[status(thm)],[f1225,f1004])).
% 0.12/0.91 fof(f1344,plain,(
% 0.12/0.91 ~sQ45_spl|~sQ43_spl|~sQ44_spl),
% 0.12/0.91 inference(split_clause,[status(thm)],[f1336,f1228,f1220,f1224])).
% 0.12/0.91 fof(f1376,plain,(
% 0.12/0.91 $false),
% 0.12/0.91 inference(sat_refutation,[status(thm)],[f1090,f1092,f1094,f1096,f1103,f1223,f1227,f1231,f1344])).
% 0.12/0.91 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.92 % Elapsed time: 0.340571 seconds
% 0.12/0.92 % CPU time: 2.397583 seconds
% 0.12/0.92 % Total memory used: 135.179 MB
% 0.12/0.92 % Net memory used: 132.743 MB
%------------------------------------------------------------------------------