%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS108+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 : n020.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:16 PM UTC 2026
% Result : Unsatisfiable 0.09s 10.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS108+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/10.37 % Computer : n020.cluster.edu
% 0.09/10.37 % Model : x86_64 x86_64
% 0.09/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.37 % Memory : 8046.5625MB
% 0.09/10.37 % OS : Linux 6.8.0-71-generic
% 0.09/10.37 % CPULimit : 300
% 0.09/10.37 % WCLimit : 300
% 0.09/10.37 % DateTime : Sun Sep 20 22:54:58 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.09/10.38 % Drodi V4.1.1
% 0.09/10.40 % Refutation found
% 0.09/10.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/10.40 % SZS output start CNFRefutation for theBenchmark
% 0.09/10.40 fof(f42,axiom,(
% 0.09/10.40 (! [X] :( cUnsatisfiable(X)<=> ( (? [Y] :( rinvR(X,Y)& ca_Ax14(Y) ))& cp2(X) ) ) )),
% 0.09/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/10.40 fof(f43,axiom,(
% 0.09/10.40 (! [X] :( cp1(X)=> ca_Cx1(X) ) )),
% 0.09/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/10.40 fof(f44,axiom,(
% 0.09/10.40 (! [X] :( cp2(X)<=> (? [Y0] : ra_Px5(X,Y0) )) )),
% 0.09/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/10.40 fof(f46,axiom,(
% 0.09/10.40 (! [X] :( cp2xcomp(X)<=> ~ (? [Y] : ra_Px5(X,Y) )) )),
% 0.09/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/10.40 fof(f55,axiom,(
% 0.09/10.40 (! [X] :( ca_Ax14(X)<=> ( (? [Y] :( rr(X,Y)& cp1(Y) ))& (! [Y0,Y1] :( ( rr(X,Y0)& rr(X,Y1) )=> Y0 = Y1 ) )) ) )),
% 0.09/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/10.40 fof(f56,axiom,(
% 0.09/10.40 (! [X] :( ca_Cx1(X)<=> ( cp2xcomp(X)& cp5xcomp(X)& cp3xcomp(X)& cp4xcomp(X) ) ) )),
% 0.09/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.40 fof(f57,axiom,(
% 0.15/10.40 (! [X] :( ca_Cx1(X)<=> (? [Y0] : ra_Px1(X,Y0) )) )),
% 0.15/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.40 fof(f58,axiom,(
% 0.15/10.40 (! [X] :( ca_Cx1xcomp(X)<=> ~ (? [Y] : ra_Px1(X,Y) )) )),
% 0.15/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.40 fof(f65,axiom,(
% 0.15/10.40 (! [X,Y] :( rinvR(X,Y)<=> rr(Y,X) ) )),
% 0.15/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.40 fof(f66,axiom,(
% 0.15/10.40 cUnsatisfiable(i2003_11_14_17_21_04740) ),
% 0.15/10.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/10.40 fof(f191,plain,(
% 0.15/10.40 ![X]: ((~cUnsatisfiable(X)|((?[Y]: (rinvR(X,Y)&ca_Ax14(Y)))&cp2(X)))&(cUnsatisfiable(X)|((![Y]: (~rinvR(X,Y)|~ca_Ax14(Y)))|~cp2(X))))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f42])).
% 0.15/10.40 fof(f192,plain,(
% 0.15/10.40 (![X]: (~cUnsatisfiable(X)|((?[Y]: (rinvR(X,Y)&ca_Ax14(Y)))&cp2(X))))&(![X]: (cUnsatisfiable(X)|((![Y]: (~rinvR(X,Y)|~ca_Ax14(Y)))|~cp2(X))))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f191])).
% 0.15/10.40 fof(f193,plain,(
% 0.15/10.40 (![X]: (~cUnsatisfiable(X)|((rinvR(X,sK0_skl(X))&ca_Ax14(sK0_skl(X)))&cp2(X))))&(![X]: (cUnsatisfiable(X)|((![Y]: (~rinvR(X,Y)|~ca_Ax14(Y)))|~cp2(X))))),
% 0.15/10.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X))],[f192])).
% 0.15/10.40 fof(f194,plain,(
% 0.15/10.40 ![X0]: (~cUnsatisfiable(X0)|rinvR(X0,sK0_skl(X0)))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f193])).
% 0.15/10.40 fof(f195,plain,(
% 0.15/10.40 ![X0]: (~cUnsatisfiable(X0)|ca_Ax14(sK0_skl(X0)))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f193])).
% 0.15/10.40 fof(f196,plain,(
% 0.15/10.40 ![X0]: (~cUnsatisfiable(X0)|cp2(X0))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f193])).
% 0.15/10.40 fof(f198,plain,(
% 0.15/10.40 ![X]: (~cp1(X)|ca_Cx1(X))),
% 0.15/10.40 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 0.15/10.40 fof(f199,plain,(
% 0.15/10.40 ![X0]: (~cp1(X0)|ca_Cx1(X0))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f198])).
% 0.15/10.40 fof(f200,plain,(
% 0.15/10.40 ![X]: ((~cp2(X)|(?[Y0]: ra_Px5(X,Y0)))&(cp2(X)|(![Y0]: ~ra_Px5(X,Y0))))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f44])).
% 0.15/10.40 fof(f201,plain,(
% 0.15/10.40 (![X]: (~cp2(X)|(?[Y0]: ra_Px5(X,Y0))))&(![X]: (cp2(X)|(![Y0]: ~ra_Px5(X,Y0))))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f200])).
% 0.15/10.40 fof(f202,plain,(
% 0.15/10.40 (![X]: (~cp2(X)|ra_Px5(X,sK1_skl(X))))&(![X]: (cp2(X)|(![Y0]: ~ra_Px5(X,Y0))))),
% 0.15/10.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y0,sK1_skl(X))],[f201])).
% 0.15/10.40 fof(f203,plain,(
% 0.15/10.40 ![X0]: (~cp2(X0)|ra_Px5(X0,sK1_skl(X0)))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f202])).
% 0.15/10.40 fof(f207,plain,(
% 0.15/10.40 ![X]: (cp2xcomp(X)<=>(![Y]: ~ra_Px5(X,Y)))),
% 0.15/10.40 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.15/10.40 fof(f208,plain,(
% 0.15/10.40 ![X]: ((~cp2xcomp(X)|(![Y]: ~ra_Px5(X,Y)))&(cp2xcomp(X)|(?[Y]: ra_Px5(X,Y))))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f207])).
% 0.15/10.40 fof(f209,plain,(
% 0.15/10.40 (![X]: (~cp2xcomp(X)|(![Y]: ~ra_Px5(X,Y))))&(![X]: (cp2xcomp(X)|(?[Y]: ra_Px5(X,Y))))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f208])).
% 0.15/10.40 fof(f210,plain,(
% 0.15/10.40 (![X]: (~cp2xcomp(X)|(![Y]: ~ra_Px5(X,Y))))&(![X]: (cp2xcomp(X)|ra_Px5(X,sK2_skl(X))))),
% 0.15/10.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(X))],[f209])).
% 0.15/10.40 fof(f211,plain,(
% 0.15/10.40 ![X0,X1]: (~cp2xcomp(X0)|~ra_Px5(X0,X1))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f210])).
% 0.15/10.40 fof(f250,plain,(
% 0.15/10.40 ![X]: (ca_Ax14(X)<=>((?[Y]: (rr(X,Y)&cp1(Y)))&(![Y0,Y1]: ((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1))))),
% 0.15/10.40 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.15/10.40 fof(f251,plain,(
% 0.15/10.40 ![X]: ((~ca_Ax14(X)|((?[Y]: (rr(X,Y)&cp1(Y)))&(![Y0,Y1]: ((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1))))&(ca_Ax14(X)|((![Y]: (~rr(X,Y)|~cp1(Y)))|(?[Y0,Y1]: ((rr(X,Y0)&rr(X,Y1))&~Y0=Y1)))))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f250])).
% 0.15/10.40 fof(f252,plain,(
% 0.15/10.40 (![X]: (~ca_Ax14(X)|((?[Y]: (rr(X,Y)&cp1(Y)))&(![Y0,Y1]: ((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1)))))&(![X]: (ca_Ax14(X)|((![Y]: (~rr(X,Y)|~cp1(Y)))|(?[Y0,Y1]: ((rr(X,Y0)&rr(X,Y1))&~Y0=Y1)))))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f251])).
% 0.15/10.40 fof(f253,plain,(
% 0.15/10.40 (![X]: (~ca_Ax14(X)|((rr(X,sK9_skl(X))&cp1(sK9_skl(X)))&(![Y0,Y1]: ((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1)))))&(![X]: (ca_Ax14(X)|((![Y]: (~rr(X,Y)|~cp1(Y)))|((rr(X,sK10_skl(X))&rr(X,sK11_skl(X)))&~sK10_skl(X)=sK11_skl(X)))))),
% 0.15/10.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(Y,sK9_skl(X)),skolemize(Y0,sK10_skl(X)),skolemize(Y1,sK11_skl(X))],[f252])).
% 0.15/10.40 fof(f254,plain,(
% 0.15/10.40 ![X0]: (~ca_Ax14(X0)|rr(X0,sK9_skl(X0)))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f253])).
% 0.15/10.40 fof(f255,plain,(
% 0.15/10.40 ![X0]: (~ca_Ax14(X0)|cp1(sK9_skl(X0)))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f253])).
% 0.15/10.40 fof(f256,plain,(
% 0.15/10.40 ![X0,X1,X2]: (~ca_Ax14(X0)|~rr(X0,X1)|~rr(X0,X2)|X1=X2)),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f253])).
% 0.15/10.40 fof(f260,plain,(
% 0.15/10.40 ![X]: ((~ca_Cx1(X)|(((cp2xcomp(X)&cp5xcomp(X))&cp3xcomp(X))&cp4xcomp(X)))&(ca_Cx1(X)|(((~cp2xcomp(X)|~cp5xcomp(X))|~cp3xcomp(X))|~cp4xcomp(X))))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f56])).
% 0.15/10.40 fof(f261,plain,(
% 0.15/10.40 (![X]: (~ca_Cx1(X)|(((cp2xcomp(X)&cp5xcomp(X))&cp3xcomp(X))&cp4xcomp(X))))&(![X]: (ca_Cx1(X)|(((~cp2xcomp(X)|~cp5xcomp(X))|~cp3xcomp(X))|~cp4xcomp(X))))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f260])).
% 0.15/10.40 fof(f262,plain,(
% 0.15/10.40 ![X0]: (~ca_Cx1(X0)|cp2xcomp(X0))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f261])).
% 0.15/10.40 fof(f267,plain,(
% 0.15/10.40 ![X]: ((~ca_Cx1(X)|(?[Y0]: ra_Px1(X,Y0)))&(ca_Cx1(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f57])).
% 0.15/10.40 fof(f268,plain,(
% 0.15/10.40 (![X]: (~ca_Cx1(X)|(?[Y0]: ra_Px1(X,Y0))))&(![X]: (ca_Cx1(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f267])).
% 0.15/10.40 fof(f269,plain,(
% 0.15/10.40 (![X]: (~ca_Cx1(X)|ra_Px1(X,sK12_skl(X))))&(![X]: (ca_Cx1(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.15/10.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(Y0,sK12_skl(X))],[f268])).
% 0.15/10.40 fof(f270,plain,(
% 0.15/10.40 ![X0]: (~ca_Cx1(X0)|ra_Px1(X0,sK12_skl(X0)))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/10.40 fof(f271,plain,(
% 0.15/10.40 ![X0,X1]: (ca_Cx1(X0)|~ra_Px1(X0,X1))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f269])).
% 0.15/10.40 fof(f272,plain,(
% 0.15/10.40 ![X]: (ca_Cx1xcomp(X)<=>(![Y]: ~ra_Px1(X,Y)))),
% 0.15/10.40 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.15/10.40 fof(f273,plain,(
% 0.15/10.40 ![X]: ((~ca_Cx1xcomp(X)|(![Y]: ~ra_Px1(X,Y)))&(ca_Cx1xcomp(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f272])).
% 0.15/10.40 fof(f274,plain,(
% 0.15/10.40 (![X]: (~ca_Cx1xcomp(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (ca_Cx1xcomp(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f273])).
% 0.15/10.40 fof(f275,plain,(
% 0.15/10.40 (![X]: (~ca_Cx1xcomp(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (ca_Cx1xcomp(X)|ra_Px1(X,sK13_skl(X))))),
% 0.15/10.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(Y,sK13_skl(X))],[f274])).
% 0.15/10.40 fof(f276,plain,(
% 0.15/10.40 ![X0,X1]: (~ca_Cx1xcomp(X0)|~ra_Px1(X0,X1))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f275])).
% 0.15/10.40 fof(f277,plain,(
% 0.15/10.40 ![X0]: (ca_Cx1xcomp(X0)|ra_Px1(X0,sK13_skl(X0)))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f275])).
% 0.15/10.40 fof(f311,plain,(
% 0.15/10.40 ![X,Y]: ((~rinvR(X,Y)|rr(Y,X))&(rinvR(X,Y)|~rr(Y,X)))),
% 0.15/10.40 inference(NNF_transformation,[status(thm)],[f65])).
% 0.15/10.40 fof(f312,plain,(
% 0.15/10.40 (![X,Y]: (~rinvR(X,Y)|rr(Y,X)))&(![X,Y]: (rinvR(X,Y)|~rr(Y,X)))),
% 0.15/10.40 inference(miniscoping,[status(thm)],[f311])).
% 0.15/10.40 fof(f313,plain,(
% 0.15/10.40 ![X0,X1]: (~rinvR(X0,X1)|rr(X1,X0))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f312])).
% 0.15/10.40 fof(f314,plain,(
% 0.15/10.40 ![X0,X1]: (rinvR(X0,X1)|~rr(X1,X0))),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f312])).
% 0.15/10.40 fof(f315,plain,(
% 0.15/10.40 cUnsatisfiable(i2003_11_14_17_21_04740)),
% 0.15/10.40 inference(cnf_transformation,[status(thm)],[f66])).
% 0.15/10.40 fof(f332,plain,(
% 0.15/10.40 ![X0]: (~ca_Ax14(X0)|rinvR(sK9_skl(X0),X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f254,f314])).
% 0.15/10.40 fof(f333,plain,(
% 0.15/10.40 ![X0]: (ra_Px1(X0,sK12_skl(X0))|~cp1(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f270,f199])).
% 0.15/10.40 fof(f334,plain,(
% 0.15/10.40 ![X0]: (ca_Cx1xcomp(X0)|ca_Cx1(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f277,f271])).
% 0.15/10.40 fof(f337,plain,(
% 0.15/10.40 ![X0]: (ca_Cx1xcomp(X0)|cp2xcomp(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f334,f262])).
% 0.15/10.40 fof(f338,plain,(
% 0.15/10.40 ![X0,X1,X2]: (~rr(sK0_skl(X0),X1)|~rr(sK0_skl(X0),X2)|X1=X2|~cUnsatisfiable(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f256,f195])).
% 0.15/10.40 fof(f339,plain,(
% 0.15/10.40 ![X0,X1]: (ca_Cx1xcomp(X0)|~ra_Px5(X0,X1))),
% 0.15/10.40 inference(resolution,[status(thm)],[f337,f211])).
% 0.15/10.40 fof(f341,plain,(
% 0.15/10.40 ![X0]: (ca_Cx1xcomp(X0)|~cp2(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f339,f203])).
% 0.15/10.40 fof(f343,plain,(
% 0.15/10.40 ![X0]: (ca_Cx1xcomp(X0)|~cUnsatisfiable(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f341,f196])).
% 0.15/10.40 fof(f345,plain,(
% 0.15/10.40 ca_Cx1xcomp(i2003_11_14_17_21_04740)),
% 0.15/10.40 inference(resolution,[status(thm)],[f343,f315])).
% 0.15/10.40 fof(f346,plain,(
% 0.15/10.40 ![X0]: (~ra_Px1(i2003_11_14_17_21_04740,X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f345,f276])).
% 0.15/10.40 fof(f374,plain,(
% 0.15/10.40 ![X0]: (ra_Px1(sK9_skl(X0),sK12_skl(sK9_skl(X0)))|~ca_Ax14(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f333,f255])).
% 0.15/10.40 fof(f389,plain,(
% 0.15/10.40 ![X0,X1]: (~rr(sK0_skl(i2003_11_14_17_21_04740),X0)|~rr(sK0_skl(i2003_11_14_17_21_04740),X1)|X0=X1)),
% 0.15/10.40 inference(resolution,[status(thm)],[f338,f315])).
% 0.15/10.40 fof(f413,plain,(
% 0.15/10.40 ![X0]: (~ca_Ax14(X0)|ca_Cx1(sK9_skl(X0)))),
% 0.15/10.40 inference(resolution,[status(thm)],[f374,f271])).
% 0.15/10.40 fof(f416,plain,(
% 0.15/10.40 ![X0]: (ca_Cx1(sK9_skl(sK0_skl(X0)))|~cUnsatisfiable(X0))),
% 0.15/10.40 inference(resolution,[status(thm)],[f413,f195])).
% 0.15/10.40 fof(f417,plain,(
% 0.15/10.40 ca_Cx1(sK9_skl(sK0_skl(i2003_11_14_17_21_04740)))),
% 0.15/10.40 inference(resolution,[status(thm)],[f416,f315])).
% 0.15/10.40 fof(f420,plain,(
% 0.15/10.40 ra_Px1(sK9_skl(sK0_skl(i2003_11_14_17_21_04740)),sK12_skl(sK9_skl(sK0_skl(i2003_11_14_17_21_04740))))),
% 0.15/10.40 inference(resolution,[status(thm)],[f417,f270])).
% 0.15/10.40 fof(f430,plain,(
% 0.15/10.40 ![X0,X1]: (~rr(sK0_skl(i2003_11_14_17_21_04740),X0)|X0=X1|~rinvR(X1,sK0_skl(i2003_11_14_17_21_04740)))),
% 0.15/10.40 inference(resolution,[status(thm)],[f389,f313])).
% 0.15/10.40 fof(f435,plain,(
% 0.15/10.40 ![X0,X1]: (X0=X1|~rinvR(X1,sK0_skl(i2003_11_14_17_21_04740))|~rinvR(X0,sK0_skl(i2003_11_14_17_21_04740)))),
% 0.15/10.40 inference(resolution,[status(thm)],[f430,f313])).
% 0.15/10.40 fof(f439,plain,(
% 0.15/10.40 ![X0]: (X0=i2003_11_14_17_21_04740|~rinvR(X0,sK0_skl(i2003_11_14_17_21_04740))|~cUnsatisfiable(i2003_11_14_17_21_04740))),
% 0.15/10.40 inference(resolution,[status(thm)],[f435,f194])).
% 0.15/10.40 fof(f440,plain,(
% 0.15/10.40 ![X0]: (X0=i2003_11_14_17_21_04740|~rinvR(X0,sK0_skl(i2003_11_14_17_21_04740)))),
% 0.15/10.40 inference(forward_subsumption_resolution,[status(thm)],[f439,f315])).
% 0.15/10.40 fof(f443,plain,(
% 0.15/10.40 sK9_skl(sK0_skl(i2003_11_14_17_21_04740))=i2003_11_14_17_21_04740|~ca_Ax14(sK0_skl(i2003_11_14_17_21_04740))),
% 0.15/10.40 inference(resolution,[status(thm)],[f440,f332])).
% 0.15/10.40 fof(f446,plain,(
% 0.15/10.40 sK9_skl(sK0_skl(i2003_11_14_17_21_04740))=i2003_11_14_17_21_04740|~cUnsatisfiable(i2003_11_14_17_21_04740)),
% 0.15/10.40 inference(resolution,[status(thm)],[f443,f195])).
% 0.15/10.40 fof(f448,plain,(
% 0.15/10.40 ra_Px1(sK9_skl(sK0_skl(i2003_11_14_17_21_04740)),sK12_skl(i2003_11_14_17_21_04740))),
% 0.15/10.40 inference(backward_demodulation,[status(thm)],[f460,f420])).
% 0.15/10.40 fof(f460,plain,(
% 0.15/10.40 sK9_skl(sK0_skl(i2003_11_14_17_21_04740))=i2003_11_14_17_21_04740),
% 0.15/10.40 inference(forward_subsumption_resolution,[status(thm)],[f446,f315])).
% 0.15/10.40 fof(f461,plain,(
% 0.15/10.40 ra_Px1(i2003_11_14_17_21_04740,sK12_skl(i2003_11_14_17_21_04740))),
% 0.15/10.40 inference(forward_demodulation,[status(thm)],[f460,f448])).
% 0.15/10.40 fof(f462,plain,(
% 0.15/10.40 $false),
% 0.15/10.40 inference(forward_subsumption_resolution,[status(thm)],[f461,f346])).
% 0.15/10.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/10.41 % Elapsed time: 0.035277 seconds
% 0.15/10.41 % CPU time: 0.101193 seconds
% 0.15/10.41 % Total memory used: 5.625 MB
% 0.15/10.41 % Net memory used: 5.385 MB
%------------------------------------------------------------------------------