%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS116+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:17 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS116+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n015.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:57:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f3,axiom,(
% 0.13/0.40 (! [X] :( cUnsatisfiable(X)=> ca(X) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f4,axiom,(
% 0.13/0.40 (! [X] :( cUnsatisfiable(X)=> (? [Y] :( rs(X,Y)& ca_Ax2(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f5,axiom,(
% 0.13/0.40 (! [X] :( ca(X)<=> ~ (? [Y] : ra_Px1(X,Y) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f6,axiom,(
% 0.13/0.40 (! [X] :( caxcomp(X)<=> (? [Y0] : ra_Px1(X,Y0) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f7,axiom,(
% 0.13/0.40 (! [X] :( cc(X)<=> (! [Y] :( rinvR(X,Y)=> ca_Vx7(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f8,axiom,(
% 0.13/0.40 (! [X] :( ca_Ax2(X)<=> ( (! [Y] :( rp(X,Y)=> ca_Vx3(Y) ))& (! [Y] :( rp(X,Y)=> ca_Vx5(Y) ))& (! [Y] :( rr(X,Y)=> cc(Y) ))& (? [Y] :( rr(X,Y)& cowlThing(Y) ))& (? [Y] :( rp(X,Y)& cowlThing(Y) ))& (! [Y] :( rp(X,Y)=> ca_Vx4(Y) ) )) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f9,axiom,(
% 0.13/0.40 (! [X] :( ca_Vx3(X)<=> (? [Y] :( rr(X,Y)& cowlThing(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f11,axiom,(
% 0.13/0.40 (! [X] :( ca_Vx5(X)<=> (! [Y] :( rr(X,Y)=> cc(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f12,axiom,(
% 0.13/0.40 (! [X] :( ca_Vx6(X)<=> (! [Y] :( rinvS(X,Y)=> caxcomp(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f13,axiom,(
% 0.13/0.40 (! [X] :( ca_Vx7(X)<=> (! [Y] :( rinvP(X,Y)=> ca_Vx6(Y) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f14,axiom,(
% 0.13/0.40 (! [X,Y] :( rinvP(X,Y)<=> rp(Y,X) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f15,axiom,(
% 0.13/0.40 (! [X,Y] :( rinvR(X,Y)<=> rr(Y,X) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f16,axiom,(
% 0.13/0.40 (! [X,Y] :( rinvS(X,Y)<=> rs(Y,X) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f18,axiom,(
% 0.13/0.40 cUnsatisfiable(i2003_11_14_17_21_33997) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f26,plain,(
% 0.13/0.40 ![X]: (~cUnsatisfiable(X)|ca(X))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.13/0.40 fof(f27,plain,(
% 0.13/0.40 ![X0]: (~cUnsatisfiable(X0)|ca(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/0.40 fof(f28,plain,(
% 0.13/0.40 ![X]: (~cUnsatisfiable(X)|(?[Y]: (rs(X,Y)&ca_Ax2(Y))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.13/0.40 fof(f29,plain,(
% 0.13/0.40 ![X]: (~cUnsatisfiable(X)|(rs(X,sK0_skl(X))&ca_Ax2(sK0_skl(X))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X))],[f28])).
% 0.13/0.40 fof(f30,plain,(
% 0.13/0.40 ![X0]: (~cUnsatisfiable(X0)|rs(X0,sK0_skl(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.40 fof(f31,plain,(
% 0.13/0.40 ![X0]: (~cUnsatisfiable(X0)|ca_Ax2(sK0_skl(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.40 fof(f32,plain,(
% 0.13/0.40 ![X]: (ca(X)<=>(![Y]: ~ra_Px1(X,Y)))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/0.40 fof(f33,plain,(
% 0.13/0.40 ![X]: ((~ca(X)|(![Y]: ~ra_Px1(X,Y)))&(ca(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f32])).
% 0.13/0.40 fof(f34,plain,(
% 0.13/0.40 (![X]: (~ca(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (ca(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f33])).
% 0.13/0.40 fof(f35,plain,(
% 0.13/0.40 (![X]: (~ca(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (ca(X)|ra_Px1(X,sK1_skl(X))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(X))],[f34])).
% 0.13/0.40 fof(f36,plain,(
% 0.13/0.40 ![X0,X1]: (~ca(X0)|~ra_Px1(X0,X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f35])).
% 0.13/0.40 fof(f38,plain,(
% 0.13/0.40 ![X]: ((~caxcomp(X)|(?[Y0]: ra_Px1(X,Y0)))&(caxcomp(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f6])).
% 0.13/0.40 fof(f39,plain,(
% 0.13/0.40 (![X]: (~caxcomp(X)|(?[Y0]: ra_Px1(X,Y0))))&(![X]: (caxcomp(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f38])).
% 0.13/0.40 fof(f40,plain,(
% 0.13/0.40 (![X]: (~caxcomp(X)|ra_Px1(X,sK2_skl(X))))&(![X]: (caxcomp(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y0,sK2_skl(X))],[f39])).
% 0.13/0.40 fof(f41,plain,(
% 0.13/0.40 ![X0]: (~caxcomp(X0)|ra_Px1(X0,sK2_skl(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f40])).
% 0.13/0.40 fof(f43,plain,(
% 0.13/0.40 ![X]: (cc(X)<=>(![Y]: (~rinvR(X,Y)|ca_Vx7(Y))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.13/0.40 fof(f44,plain,(
% 0.13/0.40 ![X]: ((~cc(X)|(![Y]: (~rinvR(X,Y)|ca_Vx7(Y))))&(cc(X)|(?[Y]: (rinvR(X,Y)&~ca_Vx7(Y)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f43])).
% 0.13/0.40 fof(f45,plain,(
% 0.13/0.40 (![X]: (~cc(X)|(![Y]: (~rinvR(X,Y)|ca_Vx7(Y)))))&(![X]: (cc(X)|(?[Y]: (rinvR(X,Y)&~ca_Vx7(Y)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f44])).
% 0.13/0.40 fof(f46,plain,(
% 0.13/0.40 (![X]: (~cc(X)|(![Y]: (~rinvR(X,Y)|ca_Vx7(Y)))))&(![X]: (cc(X)|(rinvR(X,sK3_skl(X))&~ca_Vx7(sK3_skl(X)))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Y,sK3_skl(X))],[f45])).
% 0.13/0.40 fof(f47,plain,(
% 0.13/0.40 ![X0,X1]: (~cc(X0)|~rinvR(X0,X1)|ca_Vx7(X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.40 fof(f50,plain,(
% 0.13/0.40 ![X]: (ca_Ax2(X)<=>((((((![Y]: (~rp(X,Y)|ca_Vx3(Y)))&(![Y]: (~rp(X,Y)|ca_Vx5(Y))))&(![Y]: (~rr(X,Y)|cc(Y))))&(?[Y]: (rr(X,Y)&cowlThing(Y))))&(?[Y]: (rp(X,Y)&cowlThing(Y))))&(![Y]: (~rp(X,Y)|ca_Vx4(Y)))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.13/0.40 fof(f51,definition,(
% 0.13/0.40 ![X]: (sP0_prd(X)<=>(((((![Y]: (~rp(X,Y)|ca_Vx3(Y)))&(![Y]: (~rp(X,Y)|ca_Vx5(Y))))&(![Y]: (~rr(X,Y)|cc(Y))))&(?[Y]: (rr(X,Y)&cowlThing(Y))))&(?[Y]: (rp(X,Y)&cowlThing(Y)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/0.40 fof(f52,plain,(
% 0.13/0.40 ![X]: (ca_Ax2(X)<=>(sP0_prd(X)&(![Y]: (~rp(X,Y)|ca_Vx4(Y)))))),
% 0.13/0.40 inference(formula_renaming,[status(thm)],[f50,f51])).
% 0.13/0.40 fof(f53,plain,(
% 0.13/0.40 ![X]: ((~ca_Ax2(X)|(sP0_prd(X)&(![Y]: (~rp(X,Y)|ca_Vx4(Y)))))&(ca_Ax2(X)|(~sP0_prd(X)|(?[Y]: (rp(X,Y)&~ca_Vx4(Y))))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f52])).
% 0.13/0.40 fof(f54,plain,(
% 0.13/0.40 (![X]: (~ca_Ax2(X)|(sP0_prd(X)&(![Y]: (~rp(X,Y)|ca_Vx4(Y))))))&(![X]: (ca_Ax2(X)|(~sP0_prd(X)|(?[Y]: (rp(X,Y)&~ca_Vx4(Y))))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f53])).
% 0.13/0.40 fof(f55,plain,(
% 0.13/0.40 (![X]: (~ca_Ax2(X)|(sP0_prd(X)&(![Y]: (~rp(X,Y)|ca_Vx4(Y))))))&(![X]: (ca_Ax2(X)|(~sP0_prd(X)|(rp(X,sK4_skl(X))&~ca_Vx4(sK4_skl(X))))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Y,sK4_skl(X))],[f54])).
% 0.13/0.40 fof(f56,plain,(
% 0.13/0.40 ![X0]: (~ca_Ax2(X0)|sP0_prd(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f55])).
% 0.13/0.40 fof(f60,plain,(
% 0.13/0.40 ![X]: ((~ca_Vx3(X)|(?[Y]: (rr(X,Y)&cowlThing(Y))))&(ca_Vx3(X)|(![Y]: (~rr(X,Y)|~cowlThing(Y)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f9])).
% 0.13/0.40 fof(f61,plain,(
% 0.13/0.40 (![X]: (~ca_Vx3(X)|(?[Y]: (rr(X,Y)&cowlThing(Y)))))&(![X]: (ca_Vx3(X)|(![Y]: (~rr(X,Y)|~cowlThing(Y)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f60])).
% 0.13/0.40 fof(f62,plain,(
% 0.13/0.40 (![X]: (~ca_Vx3(X)|(rr(X,sK5_skl(X))&cowlThing(sK5_skl(X)))))&(![X]: (ca_Vx3(X)|(![Y]: (~rr(X,Y)|~cowlThing(Y)))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(Y,sK5_skl(X))],[f61])).
% 0.13/0.40 fof(f63,plain,(
% 0.13/0.40 ![X0]: (~ca_Vx3(X0)|rr(X0,sK5_skl(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/0.40 fof(f72,plain,(
% 0.13/0.40 ![X]: (ca_Vx5(X)<=>(![Y]: (~rr(X,Y)|cc(Y))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.13/0.40 fof(f73,plain,(
% 0.13/0.40 ![X]: ((~ca_Vx5(X)|(![Y]: (~rr(X,Y)|cc(Y))))&(ca_Vx5(X)|(?[Y]: (rr(X,Y)&~cc(Y)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f72])).
% 0.13/0.40 fof(f74,plain,(
% 0.13/0.40 (![X]: (~ca_Vx5(X)|(![Y]: (~rr(X,Y)|cc(Y)))))&(![X]: (ca_Vx5(X)|(?[Y]: (rr(X,Y)&~cc(Y)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f73])).
% 0.13/0.40 fof(f75,plain,(
% 0.13/0.40 (![X]: (~ca_Vx5(X)|(![Y]: (~rr(X,Y)|cc(Y)))))&(![X]: (ca_Vx5(X)|(rr(X,sK7_skl(X))&~cc(sK7_skl(X)))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Y,sK7_skl(X))],[f74])).
% 0.13/0.40 fof(f76,plain,(
% 0.13/0.40 ![X0,X1]: (~ca_Vx5(X0)|~rr(X0,X1)|cc(X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f75])).
% 0.13/0.40 fof(f79,plain,(
% 0.13/0.40 ![X]: (ca_Vx6(X)<=>(![Y]: (~rinvS(X,Y)|caxcomp(Y))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.13/0.40 fof(f80,plain,(
% 0.13/0.40 ![X]: ((~ca_Vx6(X)|(![Y]: (~rinvS(X,Y)|caxcomp(Y))))&(ca_Vx6(X)|(?[Y]: (rinvS(X,Y)&~caxcomp(Y)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f79])).
% 0.13/0.40 fof(f81,plain,(
% 0.13/0.40 (![X]: (~ca_Vx6(X)|(![Y]: (~rinvS(X,Y)|caxcomp(Y)))))&(![X]: (ca_Vx6(X)|(?[Y]: (rinvS(X,Y)&~caxcomp(Y)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f80])).
% 0.13/0.40 fof(f82,plain,(
% 0.13/0.40 (![X]: (~ca_Vx6(X)|(![Y]: (~rinvS(X,Y)|caxcomp(Y)))))&(![X]: (ca_Vx6(X)|(rinvS(X,sK8_skl(X))&~caxcomp(sK8_skl(X)))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Y,sK8_skl(X))],[f81])).
% 0.13/0.40 fof(f83,plain,(
% 0.13/0.40 ![X0,X1]: (~ca_Vx6(X0)|~rinvS(X0,X1)|caxcomp(X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f82])).
% 0.13/0.40 fof(f86,plain,(
% 0.13/0.40 ![X]: (ca_Vx7(X)<=>(![Y]: (~rinvP(X,Y)|ca_Vx6(Y))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.13/0.40 fof(f87,plain,(
% 0.13/0.40 ![X]: ((~ca_Vx7(X)|(![Y]: (~rinvP(X,Y)|ca_Vx6(Y))))&(ca_Vx7(X)|(?[Y]: (rinvP(X,Y)&~ca_Vx6(Y)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f86])).
% 0.13/0.40 fof(f88,plain,(
% 0.13/0.40 (![X]: (~ca_Vx7(X)|(![Y]: (~rinvP(X,Y)|ca_Vx6(Y)))))&(![X]: (ca_Vx7(X)|(?[Y]: (rinvP(X,Y)&~ca_Vx6(Y)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f87])).
% 0.13/0.40 fof(f89,plain,(
% 0.13/0.40 (![X]: (~ca_Vx7(X)|(![Y]: (~rinvP(X,Y)|ca_Vx6(Y)))))&(![X]: (ca_Vx7(X)|(rinvP(X,sK9_skl(X))&~ca_Vx6(sK9_skl(X)))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Y,sK9_skl(X))],[f88])).
% 0.13/0.40 fof(f90,plain,(
% 0.13/0.40 ![X0,X1]: (~ca_Vx7(X0)|~rinvP(X0,X1)|ca_Vx6(X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f89])).
% 0.13/0.40 fof(f93,plain,(
% 0.13/0.40 ![X,Y]: ((~rinvP(X,Y)|rp(Y,X))&(rinvP(X,Y)|~rp(Y,X)))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f14])).
% 0.13/0.40 fof(f94,plain,(
% 0.13/0.40 (![X,Y]: (~rinvP(X,Y)|rp(Y,X)))&(![X,Y]: (rinvP(X,Y)|~rp(Y,X)))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f93])).
% 0.13/0.40 fof(f96,plain,(
% 0.13/0.40 ![X0,X1]: (rinvP(X0,X1)|~rp(X1,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f94])).
% 0.13/0.40 fof(f97,plain,(
% 0.13/0.40 ![X,Y]: ((~rinvR(X,Y)|rr(Y,X))&(rinvR(X,Y)|~rr(Y,X)))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f15])).
% 0.13/0.40 fof(f98,plain,(
% 0.13/0.40 (![X,Y]: (~rinvR(X,Y)|rr(Y,X)))&(![X,Y]: (rinvR(X,Y)|~rr(Y,X)))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f97])).
% 0.13/0.41 fof(f100,plain,(
% 0.13/0.41 ![X0,X1]: (rinvR(X0,X1)|~rr(X1,X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f98])).
% 0.13/0.41 fof(f101,plain,(
% 0.13/0.41 ![X,Y]: ((~rinvS(X,Y)|rs(Y,X))&(rinvS(X,Y)|~rs(Y,X)))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f16])).
% 0.13/0.41 fof(f102,plain,(
% 0.13/0.41 (![X,Y]: (~rinvS(X,Y)|rs(Y,X)))&(![X,Y]: (rinvS(X,Y)|~rs(Y,X)))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f101])).
% 0.13/0.41 fof(f104,plain,(
% 0.13/0.41 ![X0,X1]: (rinvS(X0,X1)|~rs(X1,X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f102])).
% 0.13/0.41 fof(f108,plain,(
% 0.13/0.41 cUnsatisfiable(i2003_11_14_17_21_33997)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.41 fof(f109,definition,(
% 0.13/0.41 ![X]: (sP1_prd(X)<=>((![Y]: (~rp(X,Y)|ca_Vx3(Y)))&(![Y]: (~rp(X,Y)|ca_Vx5(Y)))))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.13/0.41 fof(f110,plain,(
% 0.13/0.41 ![X]: (sP0_prd(X)<=>(((sP1_prd(X)&(![Y]: (~rr(X,Y)|cc(Y))))&(?[Y]: (rr(X,Y)&cowlThing(Y))))&(?[Y]: (rp(X,Y)&cowlThing(Y)))))),
% 0.13/0.41 inference(formula_renaming,[status(thm)],[f51,f109])).
% 0.13/0.41 fof(f111,plain,(
% 0.13/0.41 ![X]: ((~sP0_prd(X)|(((sP1_prd(X)&(![Y]: (~rr(X,Y)|cc(Y))))&(?[Y]: (rr(X,Y)&cowlThing(Y))))&(?[Y]: (rp(X,Y)&cowlThing(Y)))))&(sP0_prd(X)|(((~sP1_prd(X)|(?[Y]: (rr(X,Y)&~cc(Y))))|(![Y]: (~rr(X,Y)|~cowlThing(Y))))|(![Y]: (~rp(X,Y)|~cowlThing(Y))))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f110])).
% 0.13/0.41 fof(f112,plain,(
% 0.13/0.41 (![X]: (~sP0_prd(X)|(((sP1_prd(X)&(![Y]: (~rr(X,Y)|cc(Y))))&(?[Y]: (rr(X,Y)&cowlThing(Y))))&(?[Y]: (rp(X,Y)&cowlThing(Y))))))&(![X]: (sP0_prd(X)|(((~sP1_prd(X)|(?[Y]: (rr(X,Y)&~cc(Y))))|(![Y]: (~rr(X,Y)|~cowlThing(Y))))|(![Y]: (~rp(X,Y)|~cowlThing(Y))))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f111])).
% 0.13/0.41 fof(f113,plain,(
% 0.13/0.41 (![X]: (~sP0_prd(X)|(((sP1_prd(X)&(![Y]: (~rr(X,Y)|cc(Y))))&(rr(X,sK10_skl(X))&cowlThing(sK10_skl(X))))&(rp(X,sK11_skl(X))&cowlThing(sK11_skl(X))))))&(![X]: (sP0_prd(X)|(((~sP1_prd(X)|(rr(X,sK12_skl(X))&~cc(sK12_skl(X))))|(![Y]: (~rr(X,Y)|~cowlThing(Y))))|(![Y]: (~rp(X,Y)|~cowlThing(Y))))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(Y,sK10_skl(X)),skolemize(Y,sK11_skl(X)),skolemize(Y,sK12_skl(X))],[f112])).
% 0.13/0.41 fof(f114,plain,(
% 0.13/0.41 ![X0]: (~sP0_prd(X0)|sP1_prd(X0))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f113])).
% 0.13/0.41 fof(f118,plain,(
% 0.13/0.41 ![X0]: (~sP0_prd(X0)|rp(X0,sK11_skl(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f113])).
% 0.13/0.41 fof(f122,plain,(
% 0.13/0.41 ![X]: ((~sP1_prd(X)|((![Y]: (~rp(X,Y)|ca_Vx3(Y)))&(![Y]: (~rp(X,Y)|ca_Vx5(Y)))))&(sP1_prd(X)|((?[Y]: (rp(X,Y)&~ca_Vx3(Y)))|(?[Y]: (rp(X,Y)&~ca_Vx5(Y))))))),
% 0.13/0.41 inference(NNF_transformation,[status(thm)],[f109])).
% 0.13/0.41 fof(f123,plain,(
% 0.13/0.41 (![X]: (~sP1_prd(X)|((![Y]: (~rp(X,Y)|ca_Vx3(Y)))&(![Y]: (~rp(X,Y)|ca_Vx5(Y))))))&(![X]: (sP1_prd(X)|((?[Y]: (rp(X,Y)&~ca_Vx3(Y)))|(?[Y]: (rp(X,Y)&~ca_Vx5(Y))))))),
% 0.13/0.41 inference(miniscoping,[status(thm)],[f122])).
% 0.13/0.41 fof(f124,plain,(
% 0.13/0.41 (![X]: (~sP1_prd(X)|((![Y]: (~rp(X,Y)|ca_Vx3(Y)))&(![Y]: (~rp(X,Y)|ca_Vx5(Y))))))&(![X]: (sP1_prd(X)|((rp(X,sK13_skl(X))&~ca_Vx3(sK13_skl(X)))|(rp(X,sK14_skl(X))&~ca_Vx5(sK14_skl(X))))))),
% 0.13/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(Y,sK13_skl(X)),skolemize(Y,sK14_skl(X))],[f123])).
% 0.13/0.41 fof(f125,plain,(
% 0.13/0.41 ![X0,X1]: (~sP1_prd(X0)|~rp(X0,X1)|ca_Vx3(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.13/0.41 fof(f126,plain,(
% 0.13/0.41 ![X0,X1]: (~sP1_prd(X0)|~rp(X0,X1)|ca_Vx5(X1))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f124])).
% 0.13/0.41 fof(f132,plain,(
% 0.13/0.41 ca(i2003_11_14_17_21_33997)),
% 0.13/0.41 inference(resolution,[status(thm)],[f27,f108])).
% 0.13/0.41 fof(f133,plain,(
% 0.13/0.41 rs(i2003_11_14_17_21_33997,sK0_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(resolution,[status(thm)],[f30,f108])).
% 0.13/0.41 fof(f134,plain,(
% 0.13/0.41 ca_Ax2(sK0_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(resolution,[status(thm)],[f31,f108])).
% 0.13/0.41 fof(f135,plain,(
% 0.13/0.41 sP0_prd(sK0_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(resolution,[status(thm)],[f134,f56])).
% 0.13/0.41 fof(f136,plain,(
% 0.13/0.41 sP1_prd(sK0_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(resolution,[status(thm)],[f135,f114])).
% 0.13/0.41 fof(f143,plain,(
% 0.13/0.41 rinvS(sK0_skl(i2003_11_14_17_21_33997),i2003_11_14_17_21_33997)),
% 0.13/0.41 inference(resolution,[status(thm)],[f133,f104])).
% 0.13/0.41 fof(f152,plain,(
% 0.13/0.41 ~ca_Vx6(sK0_skl(i2003_11_14_17_21_33997))|caxcomp(i2003_11_14_17_21_33997)),
% 0.13/0.41 inference(resolution,[status(thm)],[f83,f143])).
% 0.13/0.41 fof(f154,plain,(
% 0.13/0.41 rp(sK0_skl(i2003_11_14_17_21_33997),sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f118,f135])).
% 0.13/0.41 fof(f206,plain,(
% 0.13/0.41 ~sP1_prd(sK0_skl(i2003_11_14_17_21_33997))|ca_Vx5(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f154,f126])).
% 0.13/0.41 fof(f207,plain,(
% 0.13/0.41 ~sP1_prd(sK0_skl(i2003_11_14_17_21_33997))|ca_Vx3(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f154,f125])).
% 0.13/0.41 fof(f210,plain,(
% 0.13/0.41 rinvP(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)),sK0_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(resolution,[status(thm)],[f154,f96])).
% 0.13/0.41 fof(f212,plain,(
% 0.13/0.41 ca_Vx5(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f206,f136])).
% 0.13/0.41 fof(f213,plain,(
% 0.13/0.41 ca_Vx3(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f207,f136])).
% 0.13/0.41 fof(f219,plain,(
% 0.13/0.41 rr(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)),sK5_skl(sK11_skl(sK0_skl(i2003_11_14_17_21_33997))))),
% 0.13/0.41 inference(resolution,[status(thm)],[f213,f63])).
% 0.13/0.41 fof(f237,plain,(
% 0.13/0.41 ~ca_Vx7(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))|ca_Vx6(sK0_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(resolution,[status(thm)],[f210,f90])).
% 0.13/0.41 fof(f338,plain,(
% 0.13/0.41 ~ca_Vx5(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))|cc(sK5_skl(sK11_skl(sK0_skl(i2003_11_14_17_21_33997))))),
% 0.13/0.41 inference(resolution,[status(thm)],[f219,f76])).
% 0.13/0.41 fof(f340,plain,(
% 0.13/0.41 rinvR(sK5_skl(sK11_skl(sK0_skl(i2003_11_14_17_21_33997))),sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f219,f100])).
% 0.13/0.41 fof(f342,plain,(
% 0.13/0.41 cc(sK5_skl(sK11_skl(sK0_skl(i2003_11_14_17_21_33997))))),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f338,f212])).
% 0.13/0.41 fof(f389,plain,(
% 0.13/0.41 ~cc(sK5_skl(sK11_skl(sK0_skl(i2003_11_14_17_21_33997))))|ca_Vx7(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(resolution,[status(thm)],[f340,f47])).
% 0.13/0.41 fof(f390,plain,(
% 0.13/0.41 ca_Vx7(sK11_skl(sK0_skl(i2003_11_14_17_21_33997)))),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f389,f342])).
% 0.13/0.41 fof(f391,plain,(
% 0.13/0.41 ca_Vx6(sK0_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(backward_subsumption_resolution,[status(thm)],[f237,f390])).
% 0.13/0.41 fof(f392,plain,(
% 0.13/0.41 caxcomp(i2003_11_14_17_21_33997)),
% 0.13/0.41 inference(backward_subsumption_resolution,[status(thm)],[f152,f391])).
% 0.13/0.41 fof(f402,plain,(
% 0.13/0.41 ra_Px1(i2003_11_14_17_21_33997,sK2_skl(i2003_11_14_17_21_33997))),
% 0.13/0.41 inference(resolution,[status(thm)],[f392,f41])).
% 0.13/0.41 fof(f404,plain,(
% 0.13/0.41 ~ca(i2003_11_14_17_21_33997)),
% 0.13/0.41 inference(resolution,[status(thm)],[f402,f36])).
% 0.13/0.41 fof(f405,plain,(
% 0.13/0.41 $false),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f404,f132])).
% 0.13/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.42 % Elapsed time: 0.068261 seconds
% 0.13/0.42 % CPU time: 0.380120 seconds
% 0.13/0.42 % Total memory used: 12.767 MB
% 0.13/0.42 % Net memory used: 11.515 MB
%------------------------------------------------------------------------------