%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS081+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 : n011.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.11s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS081+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.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 22:52:40 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.11/0.56 % Refutation found
% 0.11/0.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.11/0.56 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.56 fof(f16,axiom,(
% 0.11/0.56 (! [X] :( cUnsatisfiable(X)<=> ( (? [Y] :( rr(X,Y)& cp3(Y) ))& (? [Y] :( rr(X,Y)& cp4(Y)& cp(Y) ))& (? [Y] :( rr(X,Y)& cp4(Y) ))& (? [Y] :( rr(X,Y)& cp2(Y)& cp(Y) ))& (? [Y] :( rr(X,Y)& cp5(Y) ))& (? [Y] :( rr(X,Y)& cp(Y)& cp3(Y) ))& (? [Y] :( rr(X,Y)& cp1(Y) ))& (! [Y0,Y1,Y2,Y3,Y4] :( ( rr(X,Y0)& rr(X,Y1)& rr(X,Y2)& rr(X,Y3)& rr(X,Y4) )=> ( Y0 = Y1| Y0 = Y2| Y0 = Y3| Y0 = Y4| Y1 = Y2| Y1 = Y3| Y1 = Y4| Y2 = Y3| Y2 = Y4| Y3 = Y4 ) ))& (? [Y] :( rr(X,Y)& cp1(Y)& cp(Y) ))& (? [Y] :( rr(X,Y)& cp2(Y) ) )) ) )),
% 0.11/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.56 fof(f17,axiom,(
% 0.11/0.56 (! [X] :( cp1(X)=> ~ ( cp2(X)| cp4(X)| cp5(X)| cp3(X) ) ) )),
% 0.11/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.56 fof(f18,axiom,(
% 0.11/0.56 (! [X] :( cp2(X)=> ~ ( cp4(X)| cp5(X)| cp3(X) ) ) )),
% 0.11/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.56 fof(f19,axiom,(
% 0.11/0.56 (! [X] :( cp3(X)=> ~ ( cp4(X)| cp5(X) ) ) )),
% 0.11/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.56 fof(f20,axiom,(
% 0.11/0.56 (! [X] :( cp4(X)=> ~ cp5(X) ) )),
% 0.11/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.56 fof(f21,axiom,(
% 0.11/0.56 cUnsatisfiable(i2003_11_14_17_19_24236) ),
% 0.11/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.56 fof(f68,plain,(
% 0.11/0.56 ![X]: (cUnsatisfiable(X)<=>((((((((((?[Y]: (rr(X,Y)&cp3(Y)))&(?[Y]: ((rr(X,Y)&cp4(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp4(Y))))&(?[Y]: ((rr(X,Y)&cp2(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp5(Y))))&(?[Y]: ((rr(X,Y)&cp(Y))&cp3(Y))))&(?[Y]: (rr(X,Y)&cp1(Y))))&(![Y0,Y1,Y2,Y3,Y4]: (((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|~rr(X,Y4))|(((((((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4))))&(?[Y]: ((rr(X,Y)&cp1(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp2(Y)))))),
% 0.11/0.56 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.11/0.56 fof(f69,plain,(
% 0.11/0.56 ![X]: ((~cUnsatisfiable(X)|((((((((((?[Y]: (rr(X,Y)&cp3(Y)))&(?[Y]: ((rr(X,Y)&cp4(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp4(Y))))&(?[Y]: ((rr(X,Y)&cp2(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp5(Y))))&(?[Y]: ((rr(X,Y)&cp(Y))&cp3(Y))))&(?[Y]: (rr(X,Y)&cp1(Y))))&(![Y0,Y1,Y2,Y3,Y4]: (((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|~rr(X,Y4))|(((((((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4))))&(?[Y]: ((rr(X,Y)&cp1(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp2(Y)))))&(cUnsatisfiable(X)|((((((((((![Y]: (~rr(X,Y)|~cp3(Y)))|(![Y]: ((~rr(X,Y)|~cp4(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp4(Y))))|(![Y]: ((~rr(X,Y)|~cp2(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp5(Y))))|(![Y]: ((~rr(X,Y)|~cp(Y))|~cp3(Y))))|(![Y]: (~rr(X,Y)|~cp1(Y))))|(?[Y0,Y1,Y2,Y3,Y4]: (((((rr(X,Y0)&rr(X,Y1))&rr(X,Y2))&rr(X,Y3))&rr(X,Y4))&(((((((((~Y0=Y1&~Y0=Y2)&~Y0=Y3)&~Y0=Y4)&~Y1=Y2)&~Y1=Y3)&~Y1=Y4)&~Y2=Y3)&~Y2=Y4)&~Y3=Y4))))|(![Y]: ((~rr(X,Y)|~cp1(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp2(Y))))))),
% 0.11/0.56 inference(NNF_transformation,[status(thm)],[f68])).
% 0.11/0.56 fof(f70,plain,(
% 0.11/0.56 (![X]: (~cUnsatisfiable(X)|((((((((((?[Y]: (rr(X,Y)&cp3(Y)))&(?[Y]: ((rr(X,Y)&cp4(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp4(Y))))&(?[Y]: ((rr(X,Y)&cp2(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp5(Y))))&(?[Y]: ((rr(X,Y)&cp(Y))&cp3(Y))))&(?[Y]: (rr(X,Y)&cp1(Y))))&(![Y0,Y1,Y2,Y3,Y4]: (((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|~rr(X,Y4))|(((((((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4))))&(?[Y]: ((rr(X,Y)&cp1(Y))&cp(Y))))&(?[Y]: (rr(X,Y)&cp2(Y))))))&(![X]: (cUnsatisfiable(X)|((((((((((![Y]: (~rr(X,Y)|~cp3(Y)))|(![Y]: ((~rr(X,Y)|~cp4(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp4(Y))))|(![Y]: ((~rr(X,Y)|~cp2(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp5(Y))))|(![Y]: ((~rr(X,Y)|~cp(Y))|~cp3(Y))))|(![Y]: (~rr(X,Y)|~cp1(Y))))|(?[Y0,Y1,Y2,Y3,Y4]: (((((rr(X,Y0)&rr(X,Y1))&rr(X,Y2))&rr(X,Y3))&rr(X,Y4))&(((((((((~Y0=Y1&~Y0=Y2)&~Y0=Y3)&~Y0=Y4)&~Y1=Y2)&~Y1=Y3)&~Y1=Y4)&~Y2=Y3)&~Y2=Y4)&~Y3=Y4))))|(![Y]: ((~rr(X,Y)|~cp1(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp2(Y))))))),
% 0.11/0.56 inference(miniscoping,[status(thm)],[f69])).
% 0.11/0.56 fof(f71,plain,(
% 0.11/0.56 (![X]: (~cUnsatisfiable(X)|((((((((((rr(X,sK0_skl(X))&cp3(sK0_skl(X)))&((rr(X,sK1_skl(X))&cp4(sK1_skl(X)))&cp(sK1_skl(X))))&(rr(X,sK2_skl(X))&cp4(sK2_skl(X))))&((rr(X,sK3_skl(X))&cp2(sK3_skl(X)))&cp(sK3_skl(X))))&(rr(X,sK4_skl(X))&cp5(sK4_skl(X))))&((rr(X,sK5_skl(X))&cp(sK5_skl(X)))&cp3(sK5_skl(X))))&(rr(X,sK6_skl(X))&cp1(sK6_skl(X))))&(![Y0,Y1,Y2,Y3,Y4]: (((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|~rr(X,Y4))|(((((((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4))))&((rr(X,sK7_skl(X))&cp1(sK7_skl(X)))&cp(sK7_skl(X))))&(rr(X,sK8_skl(X))&cp2(sK8_skl(X))))))&(![X]: (cUnsatisfiable(X)|((((((((((![Y]: (~rr(X,Y)|~cp3(Y)))|(![Y]: ((~rr(X,Y)|~cp4(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp4(Y))))|(![Y]: ((~rr(X,Y)|~cp2(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp5(Y))))|(![Y]: ((~rr(X,Y)|~cp(Y))|~cp3(Y))))|(![Y]: (~rr(X,Y)|~cp1(Y))))|(((((rr(X,sK9_skl(X))&rr(X,sK10_skl(X)))&rr(X,sK11_skl(X)))&rr(X,sK12_skl(X)))&rr(X,sK13_skl(X)))&(((((((((~sK9_skl(X)=sK10_skl(X)&~sK9_skl(X)=sK11_skl(X))&~sK9_skl(X)=sK12_skl(X))&~sK9_skl(X)=sK13_skl(X))&~sK10_skl(X)=sK11_skl(X))&~sK10_skl(X)=sK12_skl(X))&~sK10_skl(X)=sK13_skl(X))&~sK11_skl(X)=sK12_skl(X))&~sK11_skl(X)=sK13_skl(X))&~sK12_skl(X)=sK13_skl(X))))|(![Y]: ((~rr(X,Y)|~cp1(Y))|~cp(Y))))|(![Y]: (~rr(X,Y)|~cp2(Y))))))),
% 0.11/0.56 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,sK11_skl,sK12_skl,sK13_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(Y,sK7_skl(X)),skolemize(Y,sK8_skl(X)),skolemize(Y0,sK9_skl(X)),skolemize(Y1,sK10_skl(X)),skolemize(Y2,sK11_skl(X)),skolemize(Y3,sK12_skl(X)),skolemize(Y4,sK13_skl(X))],[f70])).
% 0.11/0.56 fof(f72,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK0_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f73,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|cp3(sK0_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f74,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK1_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f75,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|cp4(sK1_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f79,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK3_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f80,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|cp2(sK3_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f82,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK4_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f83,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|cp5(sK4_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f87,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK6_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f88,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|cp1(sK6_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f89,plain,(
% 0.11/0.56 ![X0,X1,X2,X3,X4,X5]: (~cUnsatisfiable(X0)|~rr(X0,X1)|~rr(X0,X2)|~rr(X0,X3)|~rr(X0,X4)|~rr(X0,X5)|X1=X2|X1=X3|X1=X4|X1=X5|X2=X3|X2=X4|X2=X5|X3=X4|X3=X5|X4=X5)),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f93,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK8_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f94,plain,(
% 0.11/0.56 ![X0]: (~cUnsatisfiable(X0)|cp2(sK8_skl(X0)))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f71])).
% 0.11/0.56 fof(f110,plain,(
% 0.11/0.56 ![X]: (~cp1(X)|(((~cp2(X)&~cp4(X))&~cp5(X))&~cp3(X)))),
% 0.11/0.56 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.11/0.56 fof(f111,plain,(
% 0.11/0.56 ![X0]: (~cp1(X0)|~cp2(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.56 fof(f112,plain,(
% 0.11/0.56 ![X0]: (~cp1(X0)|~cp4(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.56 fof(f113,plain,(
% 0.11/0.56 ![X0]: (~cp1(X0)|~cp5(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.56 fof(f114,plain,(
% 0.11/0.56 ![X0]: (~cp1(X0)|~cp3(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f110])).
% 0.11/0.56 fof(f115,plain,(
% 0.11/0.56 ![X]: (~cp2(X)|((~cp4(X)&~cp5(X))&~cp3(X)))),
% 0.11/0.56 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.11/0.56 fof(f116,plain,(
% 0.11/0.56 ![X0]: (~cp2(X0)|~cp4(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f115])).
% 0.11/0.56 fof(f117,plain,(
% 0.11/0.56 ![X0]: (~cp2(X0)|~cp5(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f115])).
% 0.11/0.56 fof(f118,plain,(
% 0.11/0.56 ![X0]: (~cp2(X0)|~cp3(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f115])).
% 0.11/0.56 fof(f119,plain,(
% 0.11/0.56 ![X]: (~cp3(X)|(~cp4(X)&~cp5(X)))),
% 0.11/0.56 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.11/0.56 fof(f120,plain,(
% 0.11/0.56 ![X0]: (~cp3(X0)|~cp4(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f119])).
% 0.11/0.56 fof(f121,plain,(
% 0.11/0.56 ![X0]: (~cp3(X0)|~cp5(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f119])).
% 0.11/0.56 fof(f122,plain,(
% 0.11/0.56 ![X]: (~cp4(X)|~cp5(X))),
% 0.11/0.56 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.11/0.56 fof(f123,plain,(
% 0.11/0.56 ![X0]: (~cp4(X0)|~cp5(X0))),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f122])).
% 0.11/0.56 fof(f124,plain,(
% 0.11/0.56 cUnsatisfiable(i2003_11_14_17_19_24236)),
% 0.11/0.56 inference(cnf_transformation,[status(thm)],[f21])).
% 0.11/0.56 fof(f127,plain,(
% 0.11/0.56 cp4(sK1_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f124,f75])).
% 0.11/0.56 fof(f128,plain,(
% 0.11/0.56 rr(i2003_11_14_17_19_24236,sK1_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f124,f74])).
% 0.11/0.56 fof(f129,plain,(
% 0.11/0.56 cp3(sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f124,f73])).
% 0.11/0.56 fof(f130,plain,(
% 0.11/0.56 rr(i2003_11_14_17_19_24236,sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f124,f72])).
% 0.11/0.56 fof(f133,plain,(
% 0.11/0.56 rr(i2003_11_14_17_19_24236,sK3_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f79,f124])).
% 0.11/0.56 fof(f134,plain,(
% 0.11/0.56 cp2(sK3_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f80,f124])).
% 0.11/0.56 fof(f136,plain,(
% 0.11/0.56 rr(i2003_11_14_17_19_24236,sK4_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f82,f124])).
% 0.11/0.56 fof(f137,plain,(
% 0.11/0.56 cp5(sK4_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f83,f124])).
% 0.11/0.56 fof(f141,plain,(
% 0.11/0.56 rr(i2003_11_14_17_19_24236,sK6_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f87,f124])).
% 0.11/0.56 fof(f142,plain,(
% 0.11/0.56 cp1(sK6_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f88,f124])).
% 0.11/0.56 fof(f146,plain,(
% 0.11/0.56 rr(i2003_11_14_17_19_24236,sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f93,f124])).
% 0.11/0.56 fof(f147,plain,(
% 0.11/0.56 cp2(sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f94,f124])).
% 0.11/0.56 fof(f148,plain,(
% 0.11/0.56 ~cp3(sK1_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f127,f120])).
% 0.11/0.56 fof(f149,plain,(
% 0.11/0.56 ~cp2(sK1_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f127,f116])).
% 0.11/0.56 fof(f150,plain,(
% 0.11/0.56 ~cp1(sK1_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f127,f112])).
% 0.11/0.56 fof(f151,plain,(
% 0.11/0.56 ~cp2(sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f129,f118])).
% 0.11/0.56 fof(f152,plain,(
% 0.11/0.56 ~cp1(sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f129,f114])).
% 0.11/0.56 fof(f171,plain,(
% 0.11/0.56 ![X0,X1,X2,X3]: (~cUnsatisfiable(i2003_11_14_17_19_24236)|~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|~rr(i2003_11_14_17_19_24236,X3)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK1_skl(i2003_11_14_17_19_24236)=X3|X0=X1|X0=X2|X0=X3|X1=X2|X1=X3|X2=X3)),
% 0.11/0.56 inference(resolution,[status(thm)],[f128,f89])).
% 0.11/0.56 fof(f172,definition,(
% 0.11/0.56 sQ0_spl <=> (cUnsatisfiable(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f174,plain,(
% 0.11/0.56 ~cUnsatisfiable(i2003_11_14_17_19_24236)|sQ0_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f172])).
% 0.11/0.56 fof(f262,definition,(
% 0.11/0.56 ![X0,X1,X2,X3]: (sQ25_spl <=> (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|~rr(i2003_11_14_17_19_24236,X3)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK1_skl(i2003_11_14_17_19_24236)=X3|X0=X1|X0=X2|X0=X3|X1=X2|X1=X3|X2=X3))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f263,plain,(
% 0.11/0.56 ![X0,X1,X2,X3]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|~rr(i2003_11_14_17_19_24236,X3)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK1_skl(i2003_11_14_17_19_24236)=X3|X0=X1|X0=X2|X0=X3|X1=X2|X1=X3|X2=X3|~sQ25_spl)),
% 0.11/0.56 inference(component_clause,[status(thm)],[f262])).
% 0.11/0.56 fof(f265,plain,(
% 0.11/0.56 ~sQ0_spl|sQ25_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f171,f172,f262])).
% 0.11/0.56 fof(f266,plain,(
% 0.11/0.56 $false|sQ0_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f174,f124])).
% 0.11/0.56 fof(f267,plain,(
% 0.11/0.56 sQ0_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f266])).
% 0.11/0.56 fof(f282,plain,(
% 0.11/0.56 ~cp1(sK3_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f134,f111])).
% 0.11/0.56 fof(f372,definition,(
% 0.11/0.56 sQ36_spl <=> (sK1_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f373,plain,(
% 0.11/0.56 sK1_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|~sQ36_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f372])).
% 0.11/0.56 fof(f411,plain,(
% 0.11/0.56 ~cp3(sK0_skl(i2003_11_14_17_19_24236))|~sQ36_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f373,f148])).
% 0.11/0.56 fof(f448,plain,(
% 0.11/0.56 $false|~sQ36_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f411,f129])).
% 0.11/0.56 fof(f449,plain,(
% 0.11/0.56 ~sQ36_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f448])).
% 0.11/0.56 fof(f484,plain,(
% 0.11/0.56 ![X0,X1,X2]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|sK1_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK3_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X1|sK3_skl(i2003_11_14_17_19_24236)=X2|X0=X1|X0=X2|X1=X2|~sQ25_spl)),
% 0.11/0.56 inference(resolution,[status(thm)],[f133,f263])).
% 0.11/0.56 fof(f504,definition,(
% 0.11/0.56 sQ49_spl <=> (sK1_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f505,plain,(
% 0.11/0.56 sK1_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|~sQ49_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f504])).
% 0.11/0.56 fof(f515,definition,(
% 0.11/0.56 ![X0,X1,X2]: (sQ52_spl <=> (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK3_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X1|sK3_skl(i2003_11_14_17_19_24236)=X2|X0=X1|X0=X2|X1=X2))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f516,plain,(
% 0.11/0.56 ![X0,X1,X2]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK3_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X1|sK3_skl(i2003_11_14_17_19_24236)=X2|X0=X1|X0=X2|X1=X2|~sQ52_spl)),
% 0.11/0.56 inference(component_clause,[status(thm)],[f515])).
% 0.11/0.56 fof(f518,plain,(
% 0.11/0.56 sQ52_spl|sQ49_spl|~sQ25_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f484,f515,f504,f262])).
% 0.11/0.56 fof(f563,plain,(
% 0.11/0.56 cp2(sK1_skl(i2003_11_14_17_19_24236))|~sQ49_spl),
% 0.11/0.56 inference(forward_demodulation,[status(thm)],[f505,f134])).
% 0.11/0.56 fof(f564,plain,(
% 0.11/0.56 $false|~sQ49_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f563,f149])).
% 0.11/0.56 fof(f565,plain,(
% 0.11/0.56 ~sQ49_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f564])).
% 0.11/0.56 fof(f568,plain,(
% 0.11/0.56 ~cp4(sK4_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f137,f123])).
% 0.11/0.56 fof(f569,plain,(
% 0.11/0.56 ~cp3(sK4_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f137,f121])).
% 0.11/0.56 fof(f570,plain,(
% 0.11/0.56 ~cp2(sK4_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f137,f117])).
% 0.11/0.56 fof(f571,plain,(
% 0.11/0.56 ~cp1(sK4_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f137,f113])).
% 0.11/0.56 fof(f572,plain,(
% 0.11/0.56 ![X0,X1,X2]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|sK1_skl(i2003_11_14_17_19_24236)=sK4_skl(i2003_11_14_17_19_24236)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK4_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X1|sK4_skl(i2003_11_14_17_19_24236)=X2|X0=X1|X0=X2|X1=X2|~sQ25_spl)),
% 0.11/0.56 inference(resolution,[status(thm)],[f136,f263])).
% 0.11/0.56 fof(f590,definition,(
% 0.11/0.56 ![X0,X1,X2]: (sQ55_spl <=> (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK4_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X1|sK4_skl(i2003_11_14_17_19_24236)=X2|X0=X1|X0=X2|X1=X2))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f591,plain,(
% 0.11/0.56 ![X0,X1,X2]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|~rr(i2003_11_14_17_19_24236,X2)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK1_skl(i2003_11_14_17_19_24236)=X2|sK4_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X1|sK4_skl(i2003_11_14_17_19_24236)=X2|X0=X1|X0=X2|X1=X2|~sQ55_spl)),
% 0.11/0.56 inference(component_clause,[status(thm)],[f590])).
% 0.11/0.56 fof(f593,definition,(
% 0.11/0.56 sQ56_spl <=> (sK1_skl(i2003_11_14_17_19_24236)=sK4_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f594,plain,(
% 0.11/0.56 sK1_skl(i2003_11_14_17_19_24236)=sK4_skl(i2003_11_14_17_19_24236)|~sQ56_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f593])).
% 0.11/0.56 fof(f596,plain,(
% 0.11/0.56 sQ55_spl|sQ56_spl|~sQ25_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f572,f590,f593,f262])).
% 0.11/0.56 fof(f663,plain,(
% 0.11/0.56 ~cp4(sK1_skl(i2003_11_14_17_19_24236))|~sQ56_spl),
% 0.11/0.56 inference(forward_demodulation,[status(thm)],[f594,f568])).
% 0.11/0.56 fof(f664,plain,(
% 0.11/0.56 $false|~sQ56_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f663,f127])).
% 0.11/0.56 fof(f665,plain,(
% 0.11/0.56 ~sQ56_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f664])).
% 0.11/0.56 fof(f729,definition,(
% 0.11/0.56 sQ66_spl <=> (sK3_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f730,plain,(
% 0.11/0.56 sK3_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|~sQ66_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f729])).
% 0.11/0.56 fof(f739,plain,(
% 0.11/0.56 cp2(sK0_skl(i2003_11_14_17_19_24236))|~sQ66_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f730,f134])).
% 0.11/0.56 fof(f751,plain,(
% 0.11/0.56 $false|~sQ66_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f739,f151])).
% 0.11/0.56 fof(f752,plain,(
% 0.11/0.56 ~sQ66_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f751])).
% 0.11/0.56 fof(f759,definition,(
% 0.11/0.56 sQ68_spl <=> (sK4_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f760,plain,(
% 0.11/0.56 sK4_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|~sQ68_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f759])).
% 0.11/0.56 fof(f771,plain,(
% 0.11/0.56 ~cp3(sK0_skl(i2003_11_14_17_19_24236))|~sQ68_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f760,f569])).
% 0.11/0.56 fof(f781,plain,(
% 0.11/0.56 $false|~sQ68_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f771,f129])).
% 0.11/0.56 fof(f782,plain,(
% 0.11/0.56 ~sQ68_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f781])).
% 0.11/0.56 fof(f830,plain,(
% 0.11/0.56 ![X0,X1]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|sK1_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK4_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236)|sK4_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X1|sK6_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X1|X0=X1|~sQ55_spl)),
% 0.11/0.56 inference(resolution,[status(thm)],[f141,f591])).
% 0.11/0.56 fof(f831,plain,(
% 0.11/0.56 ![X0,X1]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|sK1_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK3_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236)|sK3_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X1|sK6_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X1|X0=X1|~sQ52_spl)),
% 0.11/0.56 inference(resolution,[status(thm)],[f141,f516])).
% 0.11/0.56 fof(f855,definition,(
% 0.11/0.56 ![X0,X1]: (sQ75_spl <=> (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK4_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X1|sK6_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X1|X0=X1))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f856,plain,(
% 0.11/0.56 ![X0,X1]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK4_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X1|sK6_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X1|X0=X1|~sQ75_spl)),
% 0.11/0.56 inference(component_clause,[status(thm)],[f855])).
% 0.11/0.56 fof(f858,definition,(
% 0.11/0.56 sQ76_spl <=> (sK1_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f859,plain,(
% 0.11/0.56 sK1_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236)|~sQ76_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f858])).
% 0.11/0.56 fof(f861,definition,(
% 0.11/0.56 sQ77_spl <=> (sK4_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f862,plain,(
% 0.11/0.56 sK4_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236)|~sQ77_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f861])).
% 0.11/0.56 fof(f864,plain,(
% 0.11/0.56 sQ75_spl|sQ76_spl|sQ77_spl|~sQ55_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f830,f855,f858,f861,f590])).
% 0.11/0.56 fof(f865,definition,(
% 0.11/0.56 ![X0,X1]: (sQ78_spl <=> (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK3_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X1|sK6_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X1|X0=X1))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f866,plain,(
% 0.11/0.56 ![X0,X1]: (~rr(i2003_11_14_17_19_24236,X0)|~rr(i2003_11_14_17_19_24236,X1)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK1_skl(i2003_11_14_17_19_24236)=X1|sK3_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X1|sK6_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X1|X0=X1|~sQ78_spl)),
% 0.11/0.56 inference(component_clause,[status(thm)],[f865])).
% 0.11/0.56 fof(f868,definition,(
% 0.11/0.56 sQ79_spl <=> (sK3_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f869,plain,(
% 0.11/0.56 sK3_skl(i2003_11_14_17_19_24236)=sK6_skl(i2003_11_14_17_19_24236)|~sQ79_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f868])).
% 0.11/0.56 fof(f871,plain,(
% 0.11/0.56 sQ78_spl|sQ76_spl|sQ79_spl|~sQ52_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f831,f865,f858,f868,f515])).
% 0.11/0.56 fof(f926,plain,(
% 0.11/0.56 cp1(sK1_skl(i2003_11_14_17_19_24236))|~sQ76_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f859,f142])).
% 0.11/0.56 fof(f967,plain,(
% 0.11/0.56 cp1(sK3_skl(i2003_11_14_17_19_24236))|~sQ79_spl),
% 0.11/0.56 inference(forward_demodulation,[status(thm)],[f869,f142])).
% 0.11/0.56 fof(f968,plain,(
% 0.11/0.56 $false|~sQ79_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f967,f282])).
% 0.11/0.56 fof(f969,plain,(
% 0.11/0.56 ~sQ79_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f968])).
% 0.11/0.56 fof(f977,plain,(
% 0.11/0.56 $false|~sQ76_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f926,f150])).
% 0.11/0.56 fof(f978,plain,(
% 0.11/0.56 ~sQ76_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f977])).
% 0.11/0.56 fof(f1068,definition,(
% 0.11/0.56 sQ100_spl <=> (sK6_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1069,plain,(
% 0.11/0.56 sK6_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|~sQ100_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1068])).
% 0.11/0.56 fof(f1075,plain,(
% 0.11/0.56 cp1(sK0_skl(i2003_11_14_17_19_24236))|~sQ100_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f1069,f142])).
% 0.11/0.56 fof(f1087,plain,(
% 0.11/0.56 $false|~sQ100_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1075,f152])).
% 0.11/0.56 fof(f1088,plain,(
% 0.11/0.56 ~sQ100_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f1087])).
% 0.11/0.56 fof(f1206,plain,(
% 0.11/0.56 ~cp1(sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 inference(resolution,[status(thm)],[f147,f111])).
% 0.11/0.56 fof(f1214,plain,(
% 0.11/0.56 ![X0]: (~rr(i2003_11_14_17_19_24236,X0)|sK1_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|sK3_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|sK6_skl(i2003_11_14_17_19_24236)=X0|sK8_skl(i2003_11_14_17_19_24236)=X0|~sQ78_spl)),
% 0.11/0.56 inference(resolution,[status(thm)],[f146,f866])).
% 0.11/0.56 fof(f1240,definition,(
% 0.11/0.56 sQ112_spl <=> (sK1_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1241,plain,(
% 0.11/0.56 sK1_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|~sQ112_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1240])).
% 0.11/0.56 fof(f1243,definition,(
% 0.11/0.56 sQ113_spl <=> (sK6_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1244,plain,(
% 0.11/0.56 sK6_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|~sQ113_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1243])).
% 0.11/0.56 fof(f1250,definition,(
% 0.11/0.56 sQ115_spl <=> (sK3_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1251,plain,(
% 0.11/0.56 sK3_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|~sQ115_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1250])).
% 0.11/0.56 fof(f1257,definition,(
% 0.11/0.56 sQ117_spl <=> (sK4_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1258,plain,(
% 0.11/0.56 sK4_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|~sQ117_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1257])).
% 0.11/0.56 fof(f1259,plain,(
% 0.11/0.56 ~sK4_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|sQ117_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1257])).
% 0.11/0.56 fof(f1260,definition,(
% 0.11/0.56 sQ118_spl <=> (sK0_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1261,plain,(
% 0.11/0.56 sK0_skl(i2003_11_14_17_19_24236)=sK8_skl(i2003_11_14_17_19_24236)|~sQ118_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1260])).
% 0.11/0.56 fof(f1283,definition,(
% 0.11/0.56 ![X0]: (sQ124_spl <=> (~rr(i2003_11_14_17_19_24236,X0)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X0|sK8_skl(i2003_11_14_17_19_24236)=X0))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1284,plain,(
% 0.11/0.56 ![X0]: (~rr(i2003_11_14_17_19_24236,X0)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK3_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X0|sK8_skl(i2003_11_14_17_19_24236)=X0|~sQ124_spl)),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1283])).
% 0.11/0.56 fof(f1286,plain,(
% 0.11/0.56 sQ124_spl|sQ112_spl|sQ115_spl|sQ113_spl|~sQ78_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f1214,f1283,f1240,f1250,f1243,f865])).
% 0.11/0.56 fof(f1331,plain,(
% 0.11/0.56 cp2(sK1_skl(i2003_11_14_17_19_24236))|~sQ112_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f1241,f147])).
% 0.11/0.56 fof(f1353,plain,(
% 0.11/0.56 $false|~sQ112_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1331,f149])).
% 0.11/0.56 fof(f1354,plain,(
% 0.11/0.56 ~sQ112_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f1353])).
% 0.11/0.56 fof(f1359,plain,(
% 0.11/0.56 ~cp1(sK6_skl(i2003_11_14_17_19_24236))|~sQ113_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f1244,f1206])).
% 0.11/0.56 fof(f1379,plain,(
% 0.11/0.56 $false|~sQ113_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1359,f142])).
% 0.11/0.56 fof(f1380,plain,(
% 0.11/0.56 ~sQ113_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f1379])).
% 0.11/0.56 fof(f1397,plain,(
% 0.11/0.56 cp2(sK4_skl(i2003_11_14_17_19_24236))|~sQ117_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f1258,f147])).
% 0.11/0.56 fof(f1420,plain,(
% 0.11/0.56 $false|~sQ117_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1397,f570])).
% 0.11/0.56 fof(f1421,plain,(
% 0.11/0.56 ~sQ117_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f1420])).
% 0.11/0.56 fof(f1445,plain,(
% 0.11/0.56 ~sK4_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|~sQ115_spl|sQ117_spl),
% 0.11/0.56 inference(forward_demodulation,[status(thm)],[f1251,f1259])).
% 0.11/0.56 fof(f1533,plain,(
% 0.11/0.56 ![X0]: (~rr(i2003_11_14_17_19_24236,X0)|sK1_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|sK4_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|sK6_skl(i2003_11_14_17_19_24236)=X0|sK0_skl(i2003_11_14_17_19_24236)=X0|~sQ75_spl)),
% 0.11/0.56 inference(resolution,[status(thm)],[f856,f130])).
% 0.11/0.56 fof(f1538,definition,(
% 0.11/0.56 ![X0]: (sQ137_spl <=> (~rr(i2003_11_14_17_19_24236,X0)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X0|sK0_skl(i2003_11_14_17_19_24236)=X0))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1539,plain,(
% 0.11/0.56 ![X0]: (~rr(i2003_11_14_17_19_24236,X0)|sK1_skl(i2003_11_14_17_19_24236)=X0|sK4_skl(i2003_11_14_17_19_24236)=X0|sK6_skl(i2003_11_14_17_19_24236)=X0|sK0_skl(i2003_11_14_17_19_24236)=X0|~sQ137_spl)),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1538])).
% 0.11/0.56 fof(f1541,plain,(
% 0.11/0.56 sQ137_spl|sQ36_spl|sQ68_spl|sQ100_spl|~sQ75_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f1533,f1538,f372,f759,f1068,f855])).
% 0.11/0.56 fof(f1613,plain,(
% 0.11/0.56 cp2(sK0_skl(i2003_11_14_17_19_24236))|~sQ118_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f1261,f147])).
% 0.11/0.56 fof(f1633,plain,(
% 0.11/0.56 $false|~sQ118_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1613,f151])).
% 0.11/0.56 fof(f1634,plain,(
% 0.11/0.56 ~sQ118_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f1633])).
% 0.11/0.56 fof(f1651,plain,(
% 0.11/0.56 sK1_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|sK3_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|sK6_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|sK8_skl(i2003_11_14_17_19_24236)=sK0_skl(i2003_11_14_17_19_24236)|~sQ124_spl),
% 0.11/0.56 inference(resolution,[status(thm)],[f1284,f130])).
% 0.11/0.56 fof(f1653,plain,(
% 0.11/0.56 sQ36_spl|sQ66_spl|sQ100_spl|sQ118_spl|~sQ124_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f1651,f372,f729,f1068,f1260,f1283])).
% 0.11/0.56 fof(f1770,plain,(
% 0.11/0.56 sK1_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|sK4_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|sK6_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|sK0_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|~sQ137_spl),
% 0.11/0.56 inference(resolution,[status(thm)],[f133,f1539])).
% 0.11/0.56 fof(f1817,definition,(
% 0.11/0.56 sQ161_spl <=> (sK4_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236))),
% 0.11/0.56 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 0.11/0.56 fof(f1818,plain,(
% 0.11/0.56 sK4_skl(i2003_11_14_17_19_24236)=sK3_skl(i2003_11_14_17_19_24236)|~sQ161_spl),
% 0.11/0.56 inference(component_clause,[status(thm)],[f1817])).
% 0.11/0.56 fof(f1831,plain,(
% 0.11/0.56 sQ49_spl|sQ161_spl|sQ79_spl|sQ66_spl|~sQ137_spl),
% 0.11/0.56 inference(split_clause,[status(thm)],[f1770,f504,f1817,f868,f729,f1538])).
% 0.11/0.56 fof(f1898,plain,(
% 0.11/0.56 $false|~sQ115_spl|sQ117_spl|~sQ161_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1818,f1445])).
% 0.11/0.56 fof(f1899,plain,(
% 0.11/0.56 ~sQ115_spl|sQ117_spl|~sQ161_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f1898])).
% 0.11/0.56 fof(f1925,plain,(
% 0.11/0.56 cp1(sK4_skl(i2003_11_14_17_19_24236))|~sQ77_spl),
% 0.11/0.56 inference(backward_demodulation,[status(thm)],[f862,f142])).
% 0.11/0.56 fof(f1953,plain,(
% 0.11/0.56 $false|~sQ77_spl),
% 0.11/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1925,f571])).
% 0.11/0.56 fof(f1954,plain,(
% 0.11/0.56 ~sQ77_spl),
% 0.11/0.56 inference(contradiction_clause,[status(thm)],[f1953])).
% 0.11/0.56 fof(f1955,plain,(
% 0.11/0.56 $false),
% 0.11/0.56 inference(sat_refutation,[status(thm)],[f265,f267,f449,f518,f565,f596,f665,f752,f782,f864,f871,f969,f978,f1088,f1286,f1354,f1380,f1421,f1541,f1634,f1653,f1831,f1899,f1954])).
% 0.11/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 1.14/0.58 % Elapsed time: 0.200940 seconds
% 1.14/0.58 % CPU time: 1.330406 seconds
% 1.14/0.58 % Total memory used: 22.460 MB
% 1.14/0.58 % Net memory used: 20.398 MB
%------------------------------------------------------------------------------