%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS107+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 : n002.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.10s 10.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS107+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.10/10.53 % Computer : n002.cluster.edu
% 0.10/10.53 % Model : x86_64 x86_64
% 0.10/10.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.53 % Memory : 8046.5625MB
% 0.10/10.53 % OS : Linux 6.8.0-71-generic
% 0.10/10.53 % CPULimit : 300
% 0.10/10.53 % WCLimit : 300
% 0.10/10.53 % DateTime : Sun Sep 20 22:56:44 UTC 2026
% 0.10/10.53 % CPUTime :
% 0.10/10.54 % Drodi V4.1.1
% 0.10/10.56 % Refutation found
% 0.10/10.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/10.56 % SZS output start CNFRefutation for theBenchmark
% 0.10/10.56 fof(f35,axiom,(
% 0.10/10.56 (! [X] :( cUnsatisfiable(X)<=> ( (? [Y] :( rrx3(X,Y)& cc1(Y) ))& (? [Y] :( rrx4(X,Y)& cc2(Y) ))& ca_Cx1(X) ) ) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f36,axiom,(
% 0.10/10.56 (! [X] :( ca_Ax2(X)<=> ( cc2(X)& cc1(X) ) ) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f37,axiom,(
% 0.10/10.56 (! [X] :( ca_Cx1(X)<=> (? [Y0] : ra_Px1(X,Y0) )) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f38,axiom,(
% 0.10/10.56 (! [X] :( ca_Cx1xcomp(X)<=> (? [Y] :( rrx3(X,Y)& ca_Ax2(Y) ) )) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f39,axiom,(
% 0.10/10.56 (! [X] :( ca_Cx1xcomp(X)<=> ~ (? [Y] : ra_Px1(X,Y) )) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f40,axiom,(
% 0.10/10.56 (! [X,Y,Z] :( ( rrx(X,Y)& rrx(X,Z) )=> Y = Z ) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f45,axiom,(
% 0.10/10.56 cUnsatisfiable(i2003_11_14_17_21_01226) ),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f50,axiom,(
% 0.10/10.56 (! [X,Y] :( rrx4(X,Y)=> rrx(X,Y) ) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f53,axiom,(
% 0.10/10.56 (! [X,Y] :( rrx3(X,Y)=> rrx(X,Y) ) )),
% 0.10/10.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/10.56 fof(f157,plain,(
% 0.10/10.56 ![X]: ((~cUnsatisfiable(X)|(((?[Y]: (rrx3(X,Y)&cc1(Y)))&(?[Y]: (rrx4(X,Y)&cc2(Y))))&ca_Cx1(X)))&(cUnsatisfiable(X)|(((![Y]: (~rrx3(X,Y)|~cc1(Y)))|(![Y]: (~rrx4(X,Y)|~cc2(Y))))|~ca_Cx1(X))))),
% 0.10/10.56 inference(NNF_transformation,[status(thm)],[f35])).
% 0.10/10.56 fof(f158,plain,(
% 0.10/10.56 (![X]: (~cUnsatisfiable(X)|(((?[Y]: (rrx3(X,Y)&cc1(Y)))&(?[Y]: (rrx4(X,Y)&cc2(Y))))&ca_Cx1(X))))&(![X]: (cUnsatisfiable(X)|(((![Y]: (~rrx3(X,Y)|~cc1(Y)))|(![Y]: (~rrx4(X,Y)|~cc2(Y))))|~ca_Cx1(X))))),
% 0.10/10.56 inference(miniscoping,[status(thm)],[f157])).
% 0.10/10.56 fof(f159,plain,(
% 0.10/10.56 (![X]: (~cUnsatisfiable(X)|(((rrx3(X,sK0_skl(X))&cc1(sK0_skl(X)))&(rrx4(X,sK1_skl(X))&cc2(sK1_skl(X))))&ca_Cx1(X))))&(![X]: (cUnsatisfiable(X)|(((![Y]: (~rrx3(X,Y)|~cc1(Y)))|(![Y]: (~rrx4(X,Y)|~cc2(Y))))|~ca_Cx1(X))))),
% 0.10/10.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl(X)),skolemize(Y,sK1_skl(X))],[f158])).
% 0.10/10.56 fof(f160,plain,(
% 0.10/10.56 ![X0]: (~cUnsatisfiable(X0)|rrx3(X0,sK0_skl(X0)))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f159])).
% 0.10/10.56 fof(f161,plain,(
% 0.10/10.56 ![X0]: (~cUnsatisfiable(X0)|cc1(sK0_skl(X0)))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f159])).
% 0.10/10.56 fof(f162,plain,(
% 0.10/10.56 ![X0]: (~cUnsatisfiable(X0)|rrx4(X0,sK1_skl(X0)))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f159])).
% 0.10/10.56 fof(f163,plain,(
% 0.10/10.56 ![X0]: (~cUnsatisfiable(X0)|cc2(sK1_skl(X0)))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f159])).
% 0.10/10.56 fof(f164,plain,(
% 0.10/10.56 ![X0]: (~cUnsatisfiable(X0)|ca_Cx1(X0))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f159])).
% 0.10/10.56 fof(f166,plain,(
% 0.10/10.56 ![X]: ((~ca_Ax2(X)|(cc2(X)&cc1(X)))&(ca_Ax2(X)|(~cc2(X)|~cc1(X))))),
% 0.10/10.56 inference(NNF_transformation,[status(thm)],[f36])).
% 0.10/10.56 fof(f167,plain,(
% 0.10/10.56 (![X]: (~ca_Ax2(X)|(cc2(X)&cc1(X))))&(![X]: (ca_Ax2(X)|(~cc2(X)|~cc1(X))))),
% 0.10/10.56 inference(miniscoping,[status(thm)],[f166])).
% 0.10/10.56 fof(f170,plain,(
% 0.10/10.56 ![X0]: (ca_Ax2(X0)|~cc2(X0)|~cc1(X0))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f167])).
% 0.10/10.56 fof(f171,plain,(
% 0.10/10.56 ![X]: ((~ca_Cx1(X)|(?[Y0]: ra_Px1(X,Y0)))&(ca_Cx1(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.10/10.56 inference(NNF_transformation,[status(thm)],[f37])).
% 0.10/10.56 fof(f172,plain,(
% 0.10/10.56 (![X]: (~ca_Cx1(X)|(?[Y0]: ra_Px1(X,Y0))))&(![X]: (ca_Cx1(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.10/10.56 inference(miniscoping,[status(thm)],[f171])).
% 0.10/10.56 fof(f173,plain,(
% 0.10/10.56 (![X]: (~ca_Cx1(X)|ra_Px1(X,sK2_skl(X))))&(![X]: (ca_Cx1(X)|(![Y0]: ~ra_Px1(X,Y0))))),
% 0.10/10.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y0,sK2_skl(X))],[f172])).
% 0.10/10.56 fof(f174,plain,(
% 0.10/10.56 ![X0]: (~ca_Cx1(X0)|ra_Px1(X0,sK2_skl(X0)))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f173])).
% 0.10/10.56 fof(f176,plain,(
% 0.10/10.56 ![X]: ((~ca_Cx1xcomp(X)|(?[Y]: (rrx3(X,Y)&ca_Ax2(Y))))&(ca_Cx1xcomp(X)|(![Y]: (~rrx3(X,Y)|~ca_Ax2(Y)))))),
% 0.10/10.56 inference(NNF_transformation,[status(thm)],[f38])).
% 0.10/10.56 fof(f177,plain,(
% 0.10/10.56 (![X]: (~ca_Cx1xcomp(X)|(?[Y]: (rrx3(X,Y)&ca_Ax2(Y)))))&(![X]: (ca_Cx1xcomp(X)|(![Y]: (~rrx3(X,Y)|~ca_Ax2(Y)))))),
% 0.10/10.56 inference(miniscoping,[status(thm)],[f176])).
% 0.10/10.56 fof(f178,plain,(
% 0.10/10.56 (![X]: (~ca_Cx1xcomp(X)|(rrx3(X,sK3_skl(X))&ca_Ax2(sK3_skl(X)))))&(![X]: (ca_Cx1xcomp(X)|(![Y]: (~rrx3(X,Y)|~ca_Ax2(Y)))))),
% 0.10/10.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Y,sK3_skl(X))],[f177])).
% 0.10/10.56 fof(f181,plain,(
% 0.10/10.56 ![X0,X1]: (ca_Cx1xcomp(X0)|~rrx3(X0,X1)|~ca_Ax2(X1))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f178])).
% 0.10/10.56 fof(f182,plain,(
% 0.10/10.56 ![X]: (ca_Cx1xcomp(X)<=>(![Y]: ~ra_Px1(X,Y)))),
% 0.10/10.56 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.10/10.56 fof(f183,plain,(
% 0.10/10.56 ![X]: ((~ca_Cx1xcomp(X)|(![Y]: ~ra_Px1(X,Y)))&(ca_Cx1xcomp(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.10/10.56 inference(NNF_transformation,[status(thm)],[f182])).
% 0.10/10.56 fof(f184,plain,(
% 0.10/10.56 (![X]: (~ca_Cx1xcomp(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (ca_Cx1xcomp(X)|(?[Y]: ra_Px1(X,Y))))),
% 0.10/10.56 inference(miniscoping,[status(thm)],[f183])).
% 0.10/10.56 fof(f185,plain,(
% 0.10/10.56 (![X]: (~ca_Cx1xcomp(X)|(![Y]: ~ra_Px1(X,Y))))&(![X]: (ca_Cx1xcomp(X)|ra_Px1(X,sK4_skl(X))))),
% 0.10/10.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Y,sK4_skl(X))],[f184])).
% 0.10/10.56 fof(f186,plain,(
% 0.10/10.56 ![X0,X1]: (~ca_Cx1xcomp(X0)|~ra_Px1(X0,X1))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f185])).
% 0.10/10.56 fof(f188,plain,(
% 0.10/10.56 ![X,Y,Z]: ((~rrx(X,Y)|~rrx(X,Z))|Y=Z)),
% 0.10/10.56 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.10/10.56 fof(f189,plain,(
% 0.10/10.56 ![Y,Z]: ((![X]: (~rrx(X,Y)|~rrx(X,Z)))|Y=Z)),
% 0.10/10.56 inference(miniscoping,[status(thm)],[f188])).
% 0.10/10.56 fof(f190,plain,(
% 0.10/10.56 ![X0,X1,X2]: (~rrx(X0,X1)|~rrx(X0,X2)|X1=X2)),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f189])).
% 0.10/10.56 fof(f203,plain,(
% 0.10/10.56 cUnsatisfiable(i2003_11_14_17_21_01226)),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f45])).
% 0.10/10.56 fof(f212,plain,(
% 0.10/10.56 ![X,Y]: (~rrx4(X,Y)|rrx(X,Y))),
% 0.10/10.56 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.10/10.56 fof(f213,plain,(
% 0.10/10.56 ![X0,X1]: (~rrx4(X0,X1)|rrx(X0,X1))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f212])).
% 0.10/10.56 fof(f218,plain,(
% 0.10/10.56 ![X,Y]: (~rrx3(X,Y)|rrx(X,Y))),
% 0.10/10.56 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.10/10.56 fof(f219,plain,(
% 0.10/10.56 ![X0,X1]: (~rrx3(X0,X1)|rrx(X0,X1))),
% 0.10/10.56 inference(cnf_transformation,[status(thm)],[f218])).
% 0.10/10.56 fof(f221,plain,(
% 0.10/10.56 ca_Cx1(i2003_11_14_17_21_01226)),
% 0.10/10.56 inference(resolution,[status(thm)],[f164,f203])).
% 0.10/10.56 fof(f225,plain,(
% 0.10/10.56 ![X0]: (rrx(X0,sK1_skl(X0))|~cUnsatisfiable(X0))),
% 0.10/10.56 inference(resolution,[status(thm)],[f213,f162])).
% 0.10/10.56 fof(f227,plain,(
% 0.10/10.56 ![X0]: (rrx(X0,sK0_skl(X0))|~cUnsatisfiable(X0))),
% 0.10/10.56 inference(resolution,[status(thm)],[f219,f160])).
% 0.10/10.56 fof(f238,plain,(
% 0.10/10.56 rrx(i2003_11_14_17_21_01226,sK1_skl(i2003_11_14_17_21_01226))),
% 0.10/10.56 inference(resolution,[status(thm)],[f225,f203])).
% 0.10/10.56 fof(f239,plain,(
% 0.10/10.56 ![X0]: (~rrx(i2003_11_14_17_21_01226,X0)|X0=sK1_skl(i2003_11_14_17_21_01226))),
% 0.10/10.56 inference(resolution,[status(thm)],[f238,f190])).
% 0.10/10.56 fof(f241,plain,(
% 0.10/10.56 rrx(i2003_11_14_17_21_01226,sK0_skl(i2003_11_14_17_21_01226))),
% 0.10/10.56 inference(resolution,[status(thm)],[f227,f203])).
% 0.10/10.56 fof(f248,plain,(
% 0.10/10.56 sK0_skl(i2003_11_14_17_21_01226)=sK1_skl(i2003_11_14_17_21_01226)),
% 0.10/10.56 inference(resolution,[status(thm)],[f239,f241])).
% 0.10/10.56 fof(f258,plain,(
% 0.10/10.56 ~cUnsatisfiable(i2003_11_14_17_21_01226)|cc2(sK0_skl(i2003_11_14_17_21_01226))),
% 0.10/10.56 inference(paramodulation,[status(thm)],[f248,f163])).
% 0.10/10.56 fof(f261,plain,(
% 0.10/10.56 cc2(sK0_skl(i2003_11_14_17_21_01226))),
% 0.10/10.56 inference(forward_subsumption_resolution,[status(thm)],[f258,f203])).
% 0.10/10.56 fof(f262,plain,(
% 0.10/10.56 ca_Ax2(sK0_skl(i2003_11_14_17_21_01226))|~cc1(sK0_skl(i2003_11_14_17_21_01226))),
% 0.10/10.56 inference(resolution,[status(thm)],[f261,f170])).
% 0.10/10.56 fof(f284,plain,(
% 0.10/10.56 ca_Ax2(sK0_skl(i2003_11_14_17_21_01226))|~cUnsatisfiable(i2003_11_14_17_21_01226)),
% 0.10/10.56 inference(resolution,[status(thm)],[f262,f161])).
% 0.10/10.56 fof(f285,plain,(
% 0.10/10.56 ca_Ax2(sK0_skl(i2003_11_14_17_21_01226))),
% 0.10/10.56 inference(forward_subsumption_resolution,[status(thm)],[f284,f203])).
% 0.10/10.56 fof(f287,plain,(
% 0.10/10.56 ![X0]: (ca_Cx1xcomp(X0)|~rrx3(X0,sK0_skl(i2003_11_14_17_21_01226)))),
% 0.10/10.56 inference(resolution,[status(thm)],[f285,f181])).
% 0.10/10.56 fof(f290,plain,(
% 0.10/10.56 ca_Cx1xcomp(i2003_11_14_17_21_01226)|~cUnsatisfiable(i2003_11_14_17_21_01226)),
% 0.10/10.56 inference(resolution,[status(thm)],[f287,f160])).
% 0.10/10.56 fof(f291,plain,(
% 0.10/10.56 ca_Cx1xcomp(i2003_11_14_17_21_01226)),
% 0.10/10.56 inference(forward_subsumption_resolution,[status(thm)],[f290,f203])).
% 0.10/10.56 fof(f294,plain,(
% 0.10/10.56 ![X0]: (~ra_Px1(i2003_11_14_17_21_01226,X0))),
% 0.10/10.56 inference(resolution,[status(thm)],[f291,f186])).
% 0.10/10.56 fof(f296,plain,(
% 0.10/10.56 ~ca_Cx1(i2003_11_14_17_21_01226)),
% 0.10/10.56 inference(resolution,[status(thm)],[f294,f174])).
% 0.10/10.56 fof(f297,plain,(
% 0.10/10.56 $false),
% 0.10/10.56 inference(forward_subsumption_resolution,[status(thm)],[f296,f221])).
% 0.10/10.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/10.57 % Elapsed time: 0.030248 seconds
% 0.10/10.57 % CPU time: 0.085271 seconds
% 0.10/10.57 % Total memory used: 3.837 MB
% 0.10/10.57 % Net memory used: 3.641 MB
%------------------------------------------------------------------------------