%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS080+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 01:00:13 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS080+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n007.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 22:50:37 UTC 2026
% 0.12/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.41 % Refutation found
% 0.12/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.41 fof(f16,axiom,(
% 0.12/0.41 (! [X] :( cUnsatisfiable(X)<=> ( (? [Y] :( rr(X,Y)& cp(Y)& cp1(Y) ))& (? [Y] :( rr(X,Y)& cp1(Y) ))& (? [Y] :( rr(X,Y)& cp4(Y) ))& (! [Y0,Y1,Y2,Y3] :( ( rr(X,Y0)& rr(X,Y1)& rr(X,Y2)& rr(X,Y3) )=> ( Y0 = Y1| Y0 = Y2| Y0 = Y3| Y1 = Y2| Y1 = Y3| Y2 = Y3 ) ))& (? [Y] :( rr(X,Y)& cp2(Y) ))& (? [Y] :( rr(X,Y)& cp3(Y) ))& (? [Y] :( rr(X,Y)& cp(Y)& cp3(Y) ))& (? [Y] :( rr(X,Y)& cp2(Y)& cp(Y) ) )) ) )),
% 0.12/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f17,axiom,(
% 0.12/0.41 (! [X] :( cp1(X)=> ~ ( cp2(X)| cp4(X)| cp5(X)| cp3(X) ) ) )),
% 0.12/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f18,axiom,(
% 0.12/0.41 (! [X] :( cp2(X)=> ~ ( cp4(X)| cp5(X)| cp3(X) ) ) )),
% 0.12/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f19,axiom,(
% 0.12/0.41 (! [X] :( cp3(X)=> ~ ( cp4(X)| cp5(X) ) ) )),
% 0.12/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f21,axiom,(
% 0.12/0.41 cUnsatisfiable(i2003_11_14_17_19_21224) ),
% 0.12/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.41 fof(f68,plain,(
% 0.12/0.41 ![X]: (cUnsatisfiable(X)<=>((((((((?[Y]: ((rr(X,Y)&cp(Y))&cp1(Y)))&(?[Y]: (rr(X,Y)&cp1(Y))))&(?[Y]: (rr(X,Y)&cp4(Y))))&(![Y0,Y1,Y2,Y3]: ((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|(((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y1=Y2)|Y1=Y3)|Y2=Y3))))&(?[Y]: (rr(X,Y)&cp2(Y))))&(?[Y]: (rr(X,Y)&cp3(Y))))&(?[Y]: ((rr(X,Y)&cp(Y))&cp3(Y))))&(?[Y]: ((rr(X,Y)&cp2(Y))&cp(Y)))))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.12/0.41 fof(f69,plain,(
% 0.12/0.41 ![X]: ((~cUnsatisfiable(X)|((((((((?[Y]: ((rr(X,Y)&cp(Y))&cp1(Y)))&(?[Y]: (rr(X,Y)&cp1(Y))))&(?[Y]: (rr(X,Y)&cp4(Y))))&(![Y0,Y1,Y2,Y3]: ((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|(((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y1=Y2)|Y1=Y3)|Y2=Y3))))&(?[Y]: (rr(X,Y)&cp2(Y))))&(?[Y]: (rr(X,Y)&cp3(Y))))&(?[Y]: ((rr(X,Y)&cp(Y))&cp3(Y))))&(?[Y]: ((rr(X,Y)&cp2(Y))&cp(Y)))))&(cUnsatisfiable(X)|((((((((![Y]: ((~rr(X,Y)|~cp(Y))|~cp1(Y)))|(![Y]: (~rr(X,Y)|~cp1(Y))))|(![Y]: (~rr(X,Y)|~cp4(Y))))|(?[Y0,Y1,Y2,Y3]: ((((rr(X,Y0)&rr(X,Y1))&rr(X,Y2))&rr(X,Y3))&(((((~Y0=Y1&~Y0=Y2)&~Y0=Y3)&~Y1=Y2)&~Y1=Y3)&~Y2=Y3))))|(![Y]: (~rr(X,Y)|~cp2(Y))))|(![Y]: (~rr(X,Y)|~cp3(Y))))|(![Y]: ((~rr(X,Y)|~cp(Y))|~cp3(Y))))|(![Y]: ((~rr(X,Y)|~cp2(Y))|~cp(Y))))))),
% 0.12/0.41 inference(NNF_transformation,[status(thm)],[f68])).
% 0.12/0.41 fof(f70,plain,(
% 0.12/0.41 (![X]: (~cUnsatisfiable(X)|((((((((?[Y]: ((rr(X,Y)&cp(Y))&cp1(Y)))&(?[Y]: (rr(X,Y)&cp1(Y))))&(?[Y]: (rr(X,Y)&cp4(Y))))&(![Y0,Y1,Y2,Y3]: ((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|(((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y1=Y2)|Y1=Y3)|Y2=Y3))))&(?[Y]: (rr(X,Y)&cp2(Y))))&(?[Y]: (rr(X,Y)&cp3(Y))))&(?[Y]: ((rr(X,Y)&cp(Y))&cp3(Y))))&(?[Y]: ((rr(X,Y)&cp2(Y))&cp(Y))))))&(![X]: (cUnsatisfiable(X)|((((((((![Y]: ((~rr(X,Y)|~cp(Y))|~cp1(Y)))|(![Y]: (~rr(X,Y)|~cp1(Y))))|(![Y]: (~rr(X,Y)|~cp4(Y))))|(?[Y0,Y1,Y2,Y3]: ((((rr(X,Y0)&rr(X,Y1))&rr(X,Y2))&rr(X,Y3))&(((((~Y0=Y1&~Y0=Y2)&~Y0=Y3)&~Y1=Y2)&~Y1=Y3)&~Y2=Y3))))|(![Y]: (~rr(X,Y)|~cp2(Y))))|(![Y]: (~rr(X,Y)|~cp3(Y))))|(![Y]: ((~rr(X,Y)|~cp(Y))|~cp3(Y))))|(![Y]: ((~rr(X,Y)|~cp2(Y))|~cp(Y))))))),
% 0.12/0.41 inference(miniscoping,[status(thm)],[f69])).
% 0.12/0.41 fof(f71,plain,(
% 0.12/0.41 (![X]: (~cUnsatisfiable(X)|(((((((((rr(X,sK0_skl(X))&cp(sK0_skl(X)))&cp1(sK0_skl(X)))&(rr(X,sK1_skl(X))&cp1(sK1_skl(X))))&(rr(X,sK2_skl(X))&cp4(sK2_skl(X))))&(![Y0,Y1,Y2,Y3]: ((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|(((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y1=Y2)|Y1=Y3)|Y2=Y3))))&(rr(X,sK3_skl(X))&cp2(sK3_skl(X))))&(rr(X,sK4_skl(X))&cp3(sK4_skl(X))))&((rr(X,sK5_skl(X))&cp(sK5_skl(X)))&cp3(sK5_skl(X))))&((rr(X,sK6_skl(X))&cp2(sK6_skl(X)))&cp(sK6_skl(X))))))&(![X]: (cUnsatisfiable(X)|((((((((![Y]: ((~rr(X,Y)|~cp(Y))|~cp1(Y)))|(![Y]: (~rr(X,Y)|~cp1(Y))))|(![Y]: (~rr(X,Y)|~cp4(Y))))|((((rr(X,sK7_skl(X))&rr(X,sK8_skl(X)))&rr(X,sK9_skl(X)))&rr(X,sK10_skl(X)))&(((((~sK7_skl(X)=sK8_skl(X)&~sK7_skl(X)=sK9_skl(X))&~sK7_skl(X)=sK10_skl(X))&~sK8_skl(X)=sK9_skl(X))&~sK8_skl(X)=sK10_skl(X))&~sK9_skl(X)=sK10_skl(X))))|(![Y]: (~rr(X,Y)|~cp2(Y))))|(![Y]: (~rr(X,Y)|~cp3(Y))))|(![Y]: ((~rr(X,Y)|~cp(Y))|~cp3(Y))))|(![Y]: ((~rr(X,Y)|~cp2(Y))|~cp(Y))))))),
% 0.12/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(Y,sK0_skl(X)),skolemize(Y,sK1_skl(X)),skolemize(Y,sK2_skl(X)),skolemize(Y,sK3_skl(X)),skolemize(Y,sK4_skl(X)),skolemize(Y,sK5_skl(X)),skolemize(Y,sK6_skl(X)),skolemize(Y0,sK7_skl(X)),skolemize(Y1,sK8_skl(X)),skolemize(Y2,sK9_skl(X)),skolemize(Y3,sK10_skl(X))],[f70])).
% 0.12/0.41 fof(f72,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK0_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f74,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|cp1(sK0_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f77,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK2_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f78,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|cp4(sK2_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f79,plain,(
% 0.12/0.41 ![X0,X1,X2,X3,X4]: (~cUnsatisfiable(X0)|~rr(X0,X1)|~rr(X0,X2)|~rr(X0,X3)|~rr(X0,X4)|X1=X2|X1=X3|X1=X4|X2=X3|X2=X4|X3=X4)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f80,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK3_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f81,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|cp2(sK3_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f82,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK4_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f83,plain,(
% 0.12/0.41 ![X0]: (~cUnsatisfiable(X0)|cp3(sK4_skl(X0)))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.41 fof(f100,plain,(
% 0.12/0.41 ![X]: (~cp1(X)|(((~cp2(X)&~cp4(X))&~cp5(X))&~cp3(X)))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.12/0.41 fof(f101,plain,(
% 0.12/0.41 ![X0]: (~cp1(X0)|~cp2(X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.12/0.41 fof(f102,plain,(
% 0.12/0.41 ![X0]: (~cp1(X0)|~cp4(X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.12/0.41 fof(f104,plain,(
% 0.12/0.41 ![X0]: (~cp1(X0)|~cp3(X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.12/0.41 fof(f105,plain,(
% 0.12/0.41 ![X]: (~cp2(X)|((~cp4(X)&~cp5(X))&~cp3(X)))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.12/0.41 fof(f106,plain,(
% 0.12/0.41 ![X0]: (~cp2(X0)|~cp4(X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f105])).
% 0.12/0.41 fof(f108,plain,(
% 0.12/0.41 ![X0]: (~cp2(X0)|~cp3(X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f105])).
% 0.12/0.41 fof(f109,plain,(
% 0.12/0.41 ![X]: (~cp3(X)|(~cp4(X)&~cp5(X)))),
% 0.12/0.41 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.12/0.41 fof(f110,plain,(
% 0.12/0.41 ![X0]: (~cp3(X0)|~cp4(X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/0.41 fof(f114,plain,(
% 0.12/0.41 cUnsatisfiable(i2003_11_14_17_19_21224)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.41 fof(f116,plain,(
% 0.12/0.41 rr(i2003_11_14_17_19_21224,sK2_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f114,f77])).
% 0.12/0.41 fof(f119,plain,(
% 0.12/0.41 cp1(sK0_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f114,f74])).
% 0.12/0.41 fof(f121,plain,(
% 0.12/0.41 rr(i2003_11_14_17_19_21224,sK0_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f114,f72])).
% 0.12/0.41 fof(f122,plain,(
% 0.12/0.41 cp4(sK2_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f78,f114])).
% 0.12/0.41 fof(f123,plain,(
% 0.12/0.41 rr(i2003_11_14_17_19_21224,sK3_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f80,f114])).
% 0.12/0.41 fof(f124,plain,(
% 0.12/0.41 cp2(sK3_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f81,f114])).
% 0.12/0.41 fof(f125,plain,(
% 0.12/0.41 rr(i2003_11_14_17_19_21224,sK4_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f82,f114])).
% 0.12/0.41 fof(f126,plain,(
% 0.12/0.41 cp3(sK4_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f83,f114])).
% 0.12/0.41 fof(f144,definition,(
% 0.12/0.41 sQ0_spl <=> (cUnsatisfiable(i2003_11_14_17_19_21224))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f146,plain,(
% 0.12/0.41 ~cUnsatisfiable(i2003_11_14_17_19_21224)|sQ0_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f144])).
% 0.12/0.41 fof(f215,plain,(
% 0.12/0.41 $false|sQ0_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f146,f114])).
% 0.12/0.41 fof(f216,plain,(
% 0.12/0.41 sQ0_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f215])).
% 0.12/0.41 fof(f390,definition,(
% 0.12/0.41 sQ44_spl <=> (sK3_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f391,plain,(
% 0.12/0.41 sK3_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224)|~sQ44_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f390])).
% 0.12/0.41 fof(f409,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~cUnsatisfiable(i2003_11_14_17_19_21224)|~rr(i2003_11_14_17_19_21224,X0)|~rr(i2003_11_14_17_19_21224,X1)|~rr(i2003_11_14_17_19_21224,X2)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK4_skl(i2003_11_14_17_19_21224)=X1|sK4_skl(i2003_11_14_17_19_21224)=X2|X0=X1|X0=X2|X1=X2)),
% 0.12/0.41 inference(resolution,[status(thm)],[f125,f79])).
% 0.12/0.41 fof(f426,definition,(
% 0.12/0.41 ![X0,X1,X2]: (sQ47_spl <=> (~rr(i2003_11_14_17_19_21224,X0)|~rr(i2003_11_14_17_19_21224,X1)|~rr(i2003_11_14_17_19_21224,X2)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK4_skl(i2003_11_14_17_19_21224)=X1|sK4_skl(i2003_11_14_17_19_21224)=X2|X0=X1|X0=X2|X1=X2))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f427,plain,(
% 0.12/0.41 ![X0,X1,X2]: (~rr(i2003_11_14_17_19_21224,X0)|~rr(i2003_11_14_17_19_21224,X1)|~rr(i2003_11_14_17_19_21224,X2)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK4_skl(i2003_11_14_17_19_21224)=X1|sK4_skl(i2003_11_14_17_19_21224)=X2|X0=X1|X0=X2|X1=X2|~sQ47_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f426])).
% 0.12/0.41 fof(f429,plain,(
% 0.12/0.41 ~sQ0_spl|sQ47_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f409,f144,f426])).
% 0.12/0.41 fof(f442,definition,(
% 0.12/0.41 sQ51_spl <=> (sK4_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f443,plain,(
% 0.12/0.41 sK4_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224)|~sQ51_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f442])).
% 0.12/0.41 fof(f630,definition,(
% 0.12/0.41 sQ71_spl <=> (sK2_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f631,plain,(
% 0.12/0.41 sK2_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224)|~sQ71_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f630])).
% 0.12/0.41 fof(f641,plain,(
% 0.12/0.41 cp4(sK0_skl(i2003_11_14_17_19_21224))|~sQ71_spl),
% 0.12/0.41 inference(backward_demodulation,[status(thm)],[f631,f122])).
% 0.12/0.41 fof(f669,plain,(
% 0.12/0.41 cp3(sK0_skl(i2003_11_14_17_19_21224))|~sQ51_spl),
% 0.12/0.41 inference(backward_demodulation,[status(thm)],[f443,f126])).
% 0.12/0.41 fof(f721,plain,(
% 0.12/0.41 ~cp1(sK0_skl(i2003_11_14_17_19_21224))|~sQ71_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f641,f102])).
% 0.12/0.41 fof(f747,plain,(
% 0.12/0.41 $false|~sQ71_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f721,f119])).
% 0.12/0.41 fof(f748,plain,(
% 0.12/0.41 ~sQ71_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f747])).
% 0.12/0.41 fof(f796,plain,(
% 0.12/0.41 ~cp1(sK0_skl(i2003_11_14_17_19_21224))|~sQ51_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f669,f104])).
% 0.12/0.41 fof(f797,plain,(
% 0.12/0.41 $false|~sQ51_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f796,f119])).
% 0.12/0.41 fof(f798,plain,(
% 0.12/0.41 ~sQ51_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f797])).
% 0.12/0.41 fof(f803,plain,(
% 0.12/0.41 ~cp1(sK3_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f124,f101])).
% 0.12/0.41 fof(f804,plain,(
% 0.12/0.41 ![X0,X1]: (~rr(i2003_11_14_17_19_21224,X0)|~rr(i2003_11_14_17_19_21224,X1)|sK4_skl(i2003_11_14_17_19_21224)=sK3_skl(i2003_11_14_17_19_21224)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK4_skl(i2003_11_14_17_19_21224)=X1|sK3_skl(i2003_11_14_17_19_21224)=X0|sK3_skl(i2003_11_14_17_19_21224)=X1|X0=X1|~sQ47_spl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f123,f427])).
% 0.12/0.41 fof(f820,definition,(
% 0.12/0.41 ![X0,X1]: (sQ79_spl <=> (~rr(i2003_11_14_17_19_21224,X0)|~rr(i2003_11_14_17_19_21224,X1)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK4_skl(i2003_11_14_17_19_21224)=X1|sK3_skl(i2003_11_14_17_19_21224)=X0|sK3_skl(i2003_11_14_17_19_21224)=X1|X0=X1))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f821,plain,(
% 0.12/0.41 ![X0,X1]: (~rr(i2003_11_14_17_19_21224,X0)|~rr(i2003_11_14_17_19_21224,X1)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK4_skl(i2003_11_14_17_19_21224)=X1|sK3_skl(i2003_11_14_17_19_21224)=X0|sK3_skl(i2003_11_14_17_19_21224)=X1|X0=X1|~sQ79_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f820])).
% 0.12/0.41 fof(f823,definition,(
% 0.12/0.41 sQ80_spl <=> (sK4_skl(i2003_11_14_17_19_21224)=sK3_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f824,plain,(
% 0.12/0.41 sK4_skl(i2003_11_14_17_19_21224)=sK3_skl(i2003_11_14_17_19_21224)|~sQ80_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f823])).
% 0.12/0.41 fof(f826,plain,(
% 0.12/0.41 sQ79_spl|sQ80_spl|~sQ47_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f804,f820,f823,f426])).
% 0.12/0.41 fof(f833,definition,(
% 0.12/0.41 sQ83_spl <=> (sK2_skl(i2003_11_14_17_19_21224)=sK3_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f834,plain,(
% 0.12/0.41 sK2_skl(i2003_11_14_17_19_21224)=sK3_skl(i2003_11_14_17_19_21224)|~sQ83_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f833])).
% 0.12/0.41 fof(f866,plain,(
% 0.12/0.41 cp2(sK2_skl(i2003_11_14_17_19_21224))|~sQ83_spl),
% 0.12/0.41 inference(backward_demodulation,[status(thm)],[f834,f124])).
% 0.12/0.41 fof(f904,plain,(
% 0.12/0.41 cp3(sK3_skl(i2003_11_14_17_19_21224))|~sQ80_spl),
% 0.12/0.41 inference(backward_demodulation,[status(thm)],[f824,f126])).
% 0.12/0.41 fof(f913,plain,(
% 0.12/0.41 ~cp3(sK2_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f122,f110])).
% 0.12/0.41 fof(f914,plain,(
% 0.12/0.41 ~cp2(sK2_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 inference(resolution,[status(thm)],[f122,f106])).
% 0.12/0.41 fof(f935,plain,(
% 0.12/0.41 ~cp1(sK0_skl(i2003_11_14_17_19_21224))|~sQ44_spl),
% 0.12/0.41 inference(backward_demodulation,[status(thm)],[f391,f803])).
% 0.12/0.41 fof(f947,plain,(
% 0.12/0.41 $false|~sQ44_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f935,f119])).
% 0.12/0.41 fof(f948,plain,(
% 0.12/0.41 ~sQ44_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f947])).
% 0.12/0.41 fof(f949,plain,(
% 0.12/0.41 $false|~sQ83_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f866,f914])).
% 0.12/0.41 fof(f950,plain,(
% 0.12/0.41 ~sQ83_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f949])).
% 0.12/0.41 fof(f993,plain,(
% 0.12/0.41 ![X0]: (~rr(i2003_11_14_17_19_21224,X0)|sK4_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK3_skl(i2003_11_14_17_19_21224)=sK0_skl(i2003_11_14_17_19_21224)|sK3_skl(i2003_11_14_17_19_21224)=X0|sK0_skl(i2003_11_14_17_19_21224)=X0|~sQ79_spl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f821,f121])).
% 0.12/0.41 fof(f994,definition,(
% 0.12/0.41 ![X0]: (sQ86_spl <=> (~rr(i2003_11_14_17_19_21224,X0)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK3_skl(i2003_11_14_17_19_21224)=X0|sK0_skl(i2003_11_14_17_19_21224)=X0))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f995,plain,(
% 0.12/0.41 ![X0]: (~rr(i2003_11_14_17_19_21224,X0)|sK4_skl(i2003_11_14_17_19_21224)=X0|sK3_skl(i2003_11_14_17_19_21224)=X0|sK0_skl(i2003_11_14_17_19_21224)=X0|~sQ86_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f994])).
% 0.12/0.41 fof(f997,plain,(
% 0.12/0.41 sQ86_spl|sQ51_spl|sQ44_spl|~sQ79_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f993,f994,f442,f390,f820])).
% 0.12/0.41 fof(f1095,definition,(
% 0.12/0.41 sQ92_spl <=> (sK4_skl(i2003_11_14_17_19_21224)=sK2_skl(i2003_11_14_17_19_21224))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f1096,plain,(
% 0.12/0.41 sK4_skl(i2003_11_14_17_19_21224)=sK2_skl(i2003_11_14_17_19_21224)|~sQ92_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f1095])).
% 0.12/0.41 fof(f1104,plain,(
% 0.12/0.41 sK4_skl(i2003_11_14_17_19_21224)=sK2_skl(i2003_11_14_17_19_21224)|sK3_skl(i2003_11_14_17_19_21224)=sK2_skl(i2003_11_14_17_19_21224)|sK0_skl(i2003_11_14_17_19_21224)=sK2_skl(i2003_11_14_17_19_21224)|~sQ86_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f995,f116])).
% 0.12/0.41 fof(f1106,plain,(
% 0.12/0.41 sQ92_spl|sQ83_spl|sQ71_spl|~sQ86_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f1104,f1095,f833,f630,f994])).
% 0.12/0.41 fof(f1213,plain,(
% 0.12/0.41 ~cp2(sK3_skl(i2003_11_14_17_19_21224))|~sQ80_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f904,f108])).
% 0.12/0.41 fof(f1215,plain,(
% 0.12/0.41 $false|~sQ80_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1213,f124])).
% 0.12/0.41 fof(f1216,plain,(
% 0.12/0.41 ~sQ80_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f1215])).
% 0.12/0.41 fof(f1219,plain,(
% 0.12/0.41 cp3(sK2_skl(i2003_11_14_17_19_21224))|~sQ92_spl),
% 0.12/0.41 inference(forward_demodulation,[status(thm)],[f1096,f126])).
% 0.12/0.41 fof(f1220,plain,(
% 0.12/0.41 $false|~sQ92_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1219,f913])).
% 0.12/0.41 fof(f1221,plain,(
% 0.12/0.41 ~sQ92_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f1220])).
% 0.12/0.41 fof(f1222,plain,(
% 0.12/0.41 $false),
% 0.12/0.41 inference(sat_refutation,[status(thm)],[f216,f429,f748,f798,f826,f948,f950,f997,f1106,f1216,f1221])).
% 0.12/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.42 % Elapsed time: 0.063042 seconds
% 0.12/0.42 % CPU time: 0.381198 seconds
% 0.12/0.42 % Total memory used: 10.311 MB
% 0.12/0.42 % Net memory used: 9.627 MB
%------------------------------------------------------------------------------