%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS101+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 : n012.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:15 PM UTC 2026
% Result : Unsatisfiable 0.03s 15.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : KRS101+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/15.70 % Computer : n012.cluster.edu
% 0.03/15.70 % Model : x86_64 x86_64
% 0.03/15.70 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/15.70 % Memory : 8046.5625MB
% 0.03/15.70 % OS : Linux 6.8.0-71-generic
% 0.03/15.70 % CPULimit : 300
% 0.03/15.70 % WCLimit : 300
% 0.03/15.70 % DateTime : Sun Sep 20 22:53:41 UTC 2026
% 0.03/15.71 % CPUTime :
% 0.03/15.71 % Drodi V4.1.1
% 0.03/15.72 % Refutation found
% 0.03/15.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.03/15.72 % SZS output start CNFRefutation for theBenchmark
% 0.03/15.72 fof(f14,axiom,(
% 0.03/15.72 (! [X] :( cUnsatisfiable(X)<=> ( (! [Y] :( rr(X,Y)=> cd(Y) ))& (! [Y] :( rr(X,Y)=> ( ~ (? [Z0,Z1] :( rs(Y,Z0)& rs(Y,Z1)& Z0 != Z1 ))| cc(Y) ) ))& (? [Y] :( rr(X,Y)& ~ (! [Z0,Z1] :( ( rs(Y,Z0)& rs(Y,Z1) )=> Z0 = Z1 ) )) )) ) )),
% 0.03/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/15.72 fof(f15,axiom,(
% 0.03/15.72 (! [X] :( cc(X)=> ~ cd(X) ) )),
% 0.03/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/15.72 fof(f16,axiom,(
% 0.03/15.72 cUnsatisfiable(i2003_11_14_17_20_36582) ),
% 0.03/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/15.72 fof(f57,plain,(
% 0.03/15.72 ![X]: (cUnsatisfiable(X)<=>(((![Y]: (~rr(X,Y)|cd(Y)))&(![Y]: (~rr(X,Y)|((![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1))|cc(Y)))))&(?[Y]: (rr(X,Y)&(?[Z0,Z1]: ((rs(Y,Z0)&rs(Y,Z1))&~Z0=Z1))))))),
% 0.03/15.72 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.03/15.72 fof(f58,definition,(
% 0.03/15.72 ![Y]: (sP0_prd(Y)<=>((![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1))|cc(Y)))),
% 0.03/15.72 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.03/15.72 fof(f59,plain,(
% 0.03/15.72 ![X]: (cUnsatisfiable(X)<=>(((![Y]: (~rr(X,Y)|cd(Y)))&(![Y]: (~rr(X,Y)|sP0_prd(Y))))&(?[Y]: (rr(X,Y)&(?[Z0,Z1]: ((rs(Y,Z0)&rs(Y,Z1))&~Z0=Z1))))))),
% 0.03/15.72 inference(formula_renaming,[status(thm)],[f57,f58])).
% 0.03/15.72 fof(f60,plain,(
% 0.03/15.72 ![X]: ((~cUnsatisfiable(X)|(((![Y]: (~rr(X,Y)|cd(Y)))&(![Y]: (~rr(X,Y)|sP0_prd(Y))))&(?[Y]: (rr(X,Y)&(?[Z0,Z1]: ((rs(Y,Z0)&rs(Y,Z1))&~Z0=Z1))))))&(cUnsatisfiable(X)|(((?[Y]: (rr(X,Y)&~cd(Y)))|(?[Y]: (rr(X,Y)&~sP0_prd(Y))))|(![Y]: (~rr(X,Y)|(![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1)))))))),
% 0.03/15.72 inference(NNF_transformation,[status(thm)],[f59])).
% 0.03/15.72 fof(f61,plain,(
% 0.03/15.72 (![X]: (~cUnsatisfiable(X)|(((![Y]: (~rr(X,Y)|cd(Y)))&(![Y]: (~rr(X,Y)|sP0_prd(Y))))&(?[Y]: (rr(X,Y)&(?[Z0,Z1]: ((rs(Y,Z0)&rs(Y,Z1))&~Z0=Z1)))))))&(![X]: (cUnsatisfiable(X)|(((?[Y]: (rr(X,Y)&~cd(Y)))|(?[Y]: (rr(X,Y)&~sP0_prd(Y))))|(![Y]: (~rr(X,Y)|(![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1)))))))),
% 0.03/15.72 inference(miniscoping,[status(thm)],[f60])).
% 0.03/15.72 fof(f62,plain,(
% 0.03/15.72 (![X]: (~cUnsatisfiable(X)|(((![Y]: (~rr(X,Y)|cd(Y)))&(![Y]: (~rr(X,Y)|sP0_prd(Y))))&(rr(X,sK0_skl(X))&((rs(sK0_skl(X),sK1_skl(X))&rs(sK0_skl(X),sK2_skl(X)))&~sK1_skl(X)=sK2_skl(X))))))&(![X]: (cUnsatisfiable(X)|(((rr(X,sK3_skl(X))&~cd(sK3_skl(X)))|(rr(X,sK4_skl(X))&~sP0_prd(sK4_skl(X))))|(![Y]: (~rr(X,Y)|(![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1)))))))),
% 0.03/15.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl]),skolemize(Y,sK0_skl(X)),skolemize(Z0,sK1_skl(X)),skolemize(Z1,sK2_skl(X)),skolemize(Y,sK3_skl(X)),skolemize(Y,sK4_skl(X))],[f61])).
% 0.03/15.72 fof(f63,plain,(
% 0.03/15.72 ![X0,X1]: (~cUnsatisfiable(X0)|~rr(X0,X1)|cd(X1))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f62])).
% 0.03/15.72 fof(f64,plain,(
% 0.03/15.72 ![X0,X1]: (~cUnsatisfiable(X0)|~rr(X0,X1)|sP0_prd(X1))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f62])).
% 0.03/15.72 fof(f65,plain,(
% 0.03/15.72 ![X0]: (~cUnsatisfiable(X0)|rr(X0,sK0_skl(X0)))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f62])).
% 0.03/15.72 fof(f66,plain,(
% 0.03/15.72 ![X0]: (~cUnsatisfiable(X0)|rs(sK0_skl(X0),sK1_skl(X0)))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f62])).
% 0.03/15.72 fof(f67,plain,(
% 0.03/15.72 ![X0]: (~cUnsatisfiable(X0)|rs(sK0_skl(X0),sK2_skl(X0)))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f62])).
% 0.03/15.72 fof(f68,plain,(
% 0.03/15.72 ![X0]: (~cUnsatisfiable(X0)|~sK1_skl(X0)=sK2_skl(X0))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f62])).
% 0.03/15.72 fof(f73,plain,(
% 0.03/15.72 ![X]: (~cc(X)|~cd(X))),
% 0.03/15.72 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.03/15.72 fof(f74,plain,(
% 0.03/15.72 ![X0]: (~cc(X0)|~cd(X0))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f73])).
% 0.03/15.72 fof(f75,plain,(
% 0.03/15.72 cUnsatisfiable(i2003_11_14_17_20_36582)),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f16])).
% 0.03/15.72 fof(f76,plain,(
% 0.03/15.72 ![Y]: ((~sP0_prd(Y)|((![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1))|cc(Y)))&(sP0_prd(Y)|((?[Z0,Z1]: ((rs(Y,Z0)&rs(Y,Z1))&~Z0=Z1))&~cc(Y))))),
% 0.03/15.72 inference(NNF_transformation,[status(thm)],[f58])).
% 0.03/15.72 fof(f77,plain,(
% 0.03/15.72 (![Y]: (~sP0_prd(Y)|((![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1))|cc(Y))))&(![Y]: (sP0_prd(Y)|((?[Z0,Z1]: ((rs(Y,Z0)&rs(Y,Z1))&~Z0=Z1))&~cc(Y))))),
% 0.03/15.72 inference(miniscoping,[status(thm)],[f76])).
% 0.03/15.72 fof(f78,plain,(
% 0.03/15.72 (![Y]: (~sP0_prd(Y)|((![Z0,Z1]: ((~rs(Y,Z0)|~rs(Y,Z1))|Z0=Z1))|cc(Y))))&(![Y]: (sP0_prd(Y)|(((rs(Y,sK5_skl(Y))&rs(Y,sK6_skl(Y)))&~sK5_skl(Y)=sK6_skl(Y))&~cc(Y))))),
% 0.03/15.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(Z0,sK5_skl(Y)),skolemize(Z1,sK6_skl(Y))],[f77])).
% 0.03/15.72 fof(f79,plain,(
% 0.03/15.72 ![X0,X1,X2]: (~sP0_prd(X0)|~rs(X0,X1)|~rs(X0,X2)|X1=X2|cc(X0))),
% 0.03/15.72 inference(cnf_transformation,[status(thm)],[f78])).
% 0.03/15.72 fof(f85,plain,(
% 0.03/15.72 ![X0]: (~rr(i2003_11_14_17_20_36582,X0)|cd(X0))),
% 0.03/15.72 inference(resolution,[status(thm)],[f63,f75])).
% 0.03/15.72 fof(f86,plain,(
% 0.03/15.72 cd(sK0_skl(i2003_11_14_17_20_36582))|~cUnsatisfiable(i2003_11_14_17_20_36582)),
% 0.03/15.72 inference(resolution,[status(thm)],[f85,f65])).
% 0.03/15.72 fof(f87,plain,(
% 0.03/15.72 cd(sK0_skl(i2003_11_14_17_20_36582))),
% 0.03/15.72 inference(forward_subsumption_resolution,[status(thm)],[f86,f75])).
% 0.03/15.72 fof(f88,plain,(
% 0.03/15.72 ~cc(sK0_skl(i2003_11_14_17_20_36582))),
% 0.03/15.72 inference(resolution,[status(thm)],[f87,f74])).
% 0.03/15.72 fof(f89,plain,(
% 0.03/15.72 ![X0]: (~rr(i2003_11_14_17_20_36582,X0)|sP0_prd(X0))),
% 0.03/15.72 inference(resolution,[status(thm)],[f64,f75])).
% 0.03/15.72 fof(f90,plain,(
% 0.03/15.72 sP0_prd(sK0_skl(i2003_11_14_17_20_36582))|~cUnsatisfiable(i2003_11_14_17_20_36582)),
% 0.03/15.72 inference(resolution,[status(thm)],[f89,f65])).
% 0.03/15.72 fof(f91,plain,(
% 0.03/15.72 sP0_prd(sK0_skl(i2003_11_14_17_20_36582))),
% 0.03/15.72 inference(forward_subsumption_resolution,[status(thm)],[f90,f75])).
% 0.03/15.72 fof(f92,plain,(
% 0.03/15.72 ![X0,X1]: (~rs(sK0_skl(i2003_11_14_17_20_36582),X0)|~rs(sK0_skl(i2003_11_14_17_20_36582),X1)|X0=X1|cc(sK0_skl(i2003_11_14_17_20_36582)))),
% 0.03/15.72 inference(resolution,[status(thm)],[f79,f91])).
% 0.03/15.72 fof(f95,plain,(
% 0.03/15.72 ![X0,X1]: (~rs(sK0_skl(i2003_11_14_17_20_36582),X0)|~rs(sK0_skl(i2003_11_14_17_20_36582),X1)|X0=X1)),
% 0.03/15.72 inference(forward_subsumption_resolution,[status(thm)],[f92,f88])).
% 0.03/15.72 fof(f96,plain,(
% 0.03/15.72 ![X0]: (~rs(sK0_skl(i2003_11_14_17_20_36582),X0)|X0=sK2_skl(i2003_11_14_17_20_36582)|~cUnsatisfiable(i2003_11_14_17_20_36582))),
% 0.03/15.72 inference(resolution,[status(thm)],[f95,f67])).
% 0.03/15.72 fof(f100,plain,(
% 0.03/15.72 ![X0]: (~rs(sK0_skl(i2003_11_14_17_20_36582),X0)|X0=sK2_skl(i2003_11_14_17_20_36582))),
% 0.03/15.72 inference(forward_subsumption_resolution,[status(thm)],[f96,f75])).
% 0.03/15.72 fof(f103,plain,(
% 0.03/15.72 sK1_skl(i2003_11_14_17_20_36582)=sK2_skl(i2003_11_14_17_20_36582)|~cUnsatisfiable(i2003_11_14_17_20_36582)),
% 0.03/15.72 inference(resolution,[status(thm)],[f100,f66])).
% 0.03/15.72 fof(f107,plain,(
% 0.03/15.72 ~cUnsatisfiable(i2003_11_14_17_20_36582)),
% 0.03/15.72 inference(forward_subsumption_resolution,[status(thm)],[f103,f68])).
% 0.03/15.72 fof(f108,plain,(
% 0.03/15.72 $false),
% 0.03/15.72 inference(backward_subsumption_resolution,[status(thm)],[f75,f107])).
% 0.03/15.72 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/15.73 % Elapsed time: 0.021914 seconds
% 0.03/15.73 % CPU time: 0.051659 seconds
% 0.03/15.73 % Total memory used: 2.501 MB
% 0.03/15.73 % Net memory used: 2.402 MB
%------------------------------------------------------------------------------