%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS110+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 : n014.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.08s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS110+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.55 % Computer : n014.cluster.edu
% 0.08/0.55 % Model : x86_64 x86_64
% 0.08/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.55 % Memory : 8046.5625MB
% 0.08/0.55 % OS : Linux 6.8.0-71-generic
% 0.08/0.55 % CPULimit : 300
% 0.08/0.55 % WCLimit : 300
% 0.08/0.55 % DateTime : Sun Sep 20 22:53:52 UTC 2026
% 0.08/0.55 % CPUTime :
% 0.08/0.56 % Drodi V4.1.1
% 0.08/0.58 % Refutation found
% 0.08/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.58 fof(f25,axiom,(
% 0.08/0.58 (! [X] :( cUnsatisfiable(X)<=> ( (? [Y] :( rs(X,Y)& ca_Ax2(Y) ))& (! [Y] :( rs(X,Y)=> cpxcomp(Y) ) )) ) )),
% 0.08/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.58 fof(f26,axiom,(
% 0.08/0.58 (! [X] :( cp(X)<=> ~ (? [Y] : ra_Px1(X,Y) )) )),
% 0.08/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.58 fof(f27,axiom,(
% 0.08/0.58 (! [X] :( cpxcomp(X)<=> (? [Y0] : ra_Px1(X,Y0) )) )),
% 0.08/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.58 fof(f28,axiom,(
% 0.08/0.58 (! [X] :( ca_Ax2(X)<=> ( cp(X)& (? [Y] :( rinvS(X,Y)& cp(Y) ) )) ) )),
% 0.08/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.58 fof(f35,axiom,(
% 0.08/0.58 cUnsatisfiable(i2003_11_14_17_21_12565) ),
% 0.08/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.58 fof(f111,plain,(
% 0.08/0.58 ![X]: (cUnsatisfiable(X)<=>((?[Y]: (rs(X,Y)&ca_Ax2(Y)))&(![Y]: (~rs(X,Y)|cpxcomp(Y)))))),
% 0.08/0.58 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.08/0.58 fof(f112,plain,(
% 0.08/0.58 ![X]: ((~cUnsatisfiable(X)|((?[Y]: (rs(X,Y)&ca_Ax2(Y)))&(![Y]: (~rs(X,Y)|cpxcomp(Y)))))&(cUnsatisfiable(X)|((![Y]: (~rs(X,Y)|~ca_Ax2(Y)))|(?[Y]: (rs(X,Y)&~cpxcomp(Y))))))),
% 0.08/0.58 inference(NNF_transformation,[status(thm)],[f111])).
% 0.08/0.58 fof(f113,plain,(
% 0.08/0.58 (![X]: (~cUnsatisfiable(X)|((?[Y]: (rs(X,Y)&ca_Ax2(Y)))&(![Y]: (~rs(X,Y)|cpxcomp(Y))))))&(![X]: (cUnsatisfiable(X)|((![Y]: (~rs(X,Y)|~ca_Ax2(Y)))|(?[Y]: (rs(X,Y)&~cpxcomp(Y))))))),
% 0.08/0.58 inference(miniscoping,[status(thm)],[f112])).
% 0.08/0.58 fof(f114,plain,(
% 0.08/0.58 (![X]: (~cUnsatisfiable(X)|((rs(X,sK0_skl(X))&ca_Ax2(sK0_skl(X)))&(![Y]: (~rs(X,Y)|cpxcomp(Y))))))&(![X]: (cUnsatisfiable(X)|((![Y]: (~rs(X,Y)|~ca_Ax2(Y)))|(rs(X,sK1_skl(X))&~cpxcomp(sK1_skl(X))))))),
% 0.08/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl(X)),skolemize(Y,sK1_skl(X))],[f113])).
% 0.08/0.58 fof(f115,plain,(
% 0.08/0.58 ![X0]: (~cUnsatisfiable(X0)|rs(X0,sK0_skl(X0)))),
% 0.08/0.58 inference(cnf_transformation,[status(thm)],[f114])).
% 0.08/0.58 fof(f116,plain,(
% 0.08/0.58 ![X0]: (~cUnsatisfiable(X0)|ca_Ax2(sK0_skl(X0)))),
% 0.08/0.58 inference(cnf_transformation,[status(thm)],[f114])).
% 0.08/0.58 fof(f117,plain,(
% 0.08/0.58 ![X0,X1]: (~cUnsatisfiable(X0)|~rs(X0,X1)|cpxcomp(X1))),
% 0.08/0.58 inference(cnf_transformation,[status(thm)],[f114])).
% 0.08/0.58 fof(f120,plain,(
% 0.08/0.58 ![X]: (cp(X)<=>(![Y]: ~ra_Px1(X,Y)))),
% 0.08/0.58 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.08/0.58 fof(f121,plain,(
% 0.08/0.58 ![X]: ((~cp(X)|(![Y]: ~ra_Px1(X,Y)))&(cp(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.08/0.58 inference(NNF_transformation,[status(thm)],[f120])).
% 0.08/0.58 fof(f122,plain,(
% 0.08/0.58 (![X]: (~cp(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (cp(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.08/0.58 inference(miniscoping,[status(thm)],[f121])).
% 0.08/0.58 fof(f123,plain,(
% 0.08/0.58 (![X]: (~cp(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (cp(X)|ra_Px1(X,sK2_skl(X))))),
% 0.08/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(X))],[f122])).
% 0.08/0.58 fof(f124,plain,(
% 0.08/0.58 ![X0,X1]: (~cp(X0)|~ra_Px1(X0,X1))),
% 0.08/0.58 inference(cnf_transformation,[status(thm)],[f123])).
% 0.08/0.58 fof(f126,plain,(
% 0.08/0.58 ![X]: ((~cpxcomp(X)|(?[Y0]: ra_Px1(X,Y0)))&(cpxcomp(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.08/0.58 inference(NNF_transformation,[status(thm)],[f27])).
% 0.08/0.58 fof(f127,plain,(
% 0.08/0.58 (![X]: (~cpxcomp(X)|(?[Y0]: ra_Px1(X,Y0))))&(![X]: (cpxcomp(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.08/0.58 inference(miniscoping,[status(thm)],[f126])).
% 0.08/0.58 fof(f128,plain,(
% 0.08/0.58 (![X]: (~cpxcomp(X)|ra_Px1(X,sK3_skl(X))))&(![X]: (cpxcomp(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.08/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Y0,sK3_skl(X))],[f127])).
% 0.08/0.58 fof(f129,plain,(
% 0.08/0.58 ![X0]: (~cpxcomp(X0)|ra_Px1(X0,sK3_skl(X0)))),
% 0.08/0.58 inference(cnf_transformation,[status(thm)],[f128])).
% 0.08/0.58 fof(f131,plain,(
% 0.08/0.58 ![X]: ((~ca_Ax2(X)|(cp(X)&(?[Y]: (rinvS(X,Y)&cp(Y)))))&(ca_Ax2(X)|(~cp(X)|(![Y]: (~rinvS(X,Y)|~cp(Y))))))),
% 0.08/0.58 inference(NNF_transformation,[status(thm)],[f28])).
% 0.08/0.58 fof(f132,plain,(
% 0.08/0.58 (![X]: (~ca_Ax2(X)|(cp(X)&(?[Y]: (rinvS(X,Y)&cp(Y))))))&(![X]: (ca_Ax2(X)|(~cp(X)|(![Y]: (~rinvS(X,Y)|~cp(Y))))))),
% 0.08/0.58 inference(miniscoping,[status(thm)],[f131])).
% 0.08/0.58 fof(f133,plain,(
% 0.08/0.58 (![X]: (~ca_Ax2(X)|(cp(X)&(rinvS(X,sK4_skl(X))&cp(sK4_skl(X))))))&(![X]: (ca_Ax2(X)|(~cp(X)|(![Y]: (~rinvS(X,Y)|~cp(Y))))))),
% 0.08/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Y,sK4_skl(X))],[f132])).
% 0.08/0.58 fof(f134,plain,(
% 0.08/0.58 ![X0]: (~ca_Ax2(X0)|cp(X0))),
% 0.08/0.58 inference(cnf_transformation,[status(thm)],[f133])).
% 0.08/0.58 fof(f159,plain,(
% 0.08/0.58 cUnsatisfiable(i2003_11_14_17_21_12565)),
% 0.08/0.58 inference(cnf_transformation,[status(thm)],[f35])).
% 0.08/0.58 fof(f165,plain,(
% 0.08/0.58 rs(i2003_11_14_17_21_12565,sK0_skl(i2003_11_14_17_21_12565))),
% 0.08/0.58 inference(resolution,[status(thm)],[f115,f159])).
% 0.08/0.58 fof(f166,plain,(
% 0.08/0.58 ca_Ax2(sK0_skl(i2003_11_14_17_21_12565))),
% 0.08/0.58 inference(resolution,[status(thm)],[f116,f159])).
% 0.08/0.58 fof(f167,plain,(
% 0.08/0.58 cp(sK0_skl(i2003_11_14_17_21_12565))),
% 0.08/0.58 inference(resolution,[status(thm)],[f166,f134])).
% 0.08/0.58 fof(f179,plain,(
% 0.08/0.58 ~cUnsatisfiable(i2003_11_14_17_21_12565)|cpxcomp(sK0_skl(i2003_11_14_17_21_12565))),
% 0.08/0.58 inference(resolution,[status(thm)],[f165,f117])).
% 0.08/0.58 fof(f180,definition,(
% 0.08/0.58 sQ0_spl <=> (cUnsatisfiable(i2003_11_14_17_21_12565))),
% 0.08/0.58 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.58 fof(f182,plain,(
% 0.08/0.58 ~cUnsatisfiable(i2003_11_14_17_21_12565)|sQ0_spl),
% 0.08/0.58 inference(component_clause,[status(thm)],[f180])).
% 0.08/0.58 fof(f194,definition,(
% 0.08/0.58 sQ4_spl <=> (cpxcomp(sK0_skl(i2003_11_14_17_21_12565)))),
% 0.08/0.58 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.08/0.58 fof(f195,plain,(
% 0.08/0.58 cpxcomp(sK0_skl(i2003_11_14_17_21_12565))|~sQ4_spl),
% 0.08/0.58 inference(component_clause,[status(thm)],[f194])).
% 0.08/0.58 fof(f197,plain,(
% 0.08/0.58 ~sQ0_spl|sQ4_spl),
% 0.08/0.58 inference(split_clause,[status(thm)],[f179,f180,f194])).
% 0.08/0.58 fof(f200,plain,(
% 0.08/0.58 ra_Px1(sK0_skl(i2003_11_14_17_21_12565),sK3_skl(sK0_skl(i2003_11_14_17_21_12565)))|~sQ4_spl),
% 0.08/0.58 inference(resolution,[status(thm)],[f195,f129])).
% 0.08/0.58 fof(f224,plain,(
% 0.08/0.58 ~cp(sK0_skl(i2003_11_14_17_21_12565))|~sQ4_spl),
% 0.08/0.58 inference(resolution,[status(thm)],[f200,f124])).
% 0.08/0.58 fof(f225,plain,(
% 0.08/0.58 $false|~sQ4_spl),
% 0.08/0.58 inference(forward_subsumption_resolution,[status(thm)],[f224,f167])).
% 0.08/0.58 fof(f226,plain,(
% 0.08/0.58 ~sQ4_spl),
% 0.08/0.58 inference(contradiction_clause,[status(thm)],[f225])).
% 0.08/0.58 fof(f227,plain,(
% 0.08/0.58 $false|sQ0_spl),
% 0.08/0.58 inference(forward_subsumption_resolution,[status(thm)],[f182,f159])).
% 0.08/0.58 fof(f228,plain,(
% 0.08/0.58 sQ0_spl),
% 0.08/0.58 inference(contradiction_clause,[status(thm)],[f227])).
% 0.08/0.58 fof(f229,plain,(
% 0.08/0.58 $false),
% 0.08/0.58 inference(sat_refutation,[status(thm)],[f197,f226,f228])).
% 0.08/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.60 % Elapsed time: 0.034920 seconds
% 0.12/0.60 % CPU time: 0.080312 seconds
% 0.12/0.60 % Total memory used: 3.078 MB
% 0.12/0.60 % Net memory used: 2.965 MB
%------------------------------------------------------------------------------