%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUN085+2 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:57:28 PM UTC 2026
% Result : Theorem 0.23s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUN085+2 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n003.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 03:27:15 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.23/0.48 % Refutation found
% 0.23/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.23/0.48 fof(f1,axiom,(
% 0.23/0.48 (? [Y24] :(! [X19] :( ( ~ r1(X19)& X19 != Y24 )| ( r1(X19)& X19 = Y24 ) ) ))),
% 0.23/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.48 fof(f2,axiom,(
% 0.23/0.48 (! [X11] :(? [Y21] :(! [X12] :( ( ~ r2(X11,X12)& X12 != Y21 )| ( r2(X11,X12)& X12 = Y21 ) ) )))),
% 0.23/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.48 fof(f3,axiom,(
% 0.23/0.48 (! [X13,X14] :(? [Y22] :(! [X15] :( ( ~ r3(X13,X14,X15)& X15 != Y22 )| ( r3(X13,X14,X15)& X15 = Y22 ) ) )))),
% 0.23/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.48 fof(f5,axiom,(
% 0.23/0.48 (! [X1,X8] :(? [Y4] :( (? [Y5] :( (? [Y15] :( r2(X8,Y15)& r3(X1,Y15,Y5) ))& Y5 = Y4 ))& (? [Y7] :( r2(Y7,Y4)& r3(X1,X8,Y7) ) )) ))),
% 0.23/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.48 fof(f11,axiom,(
% 0.23/0.48 (! [X7,Y10] :( (! [Y20] :( ~ r1(Y20)| Y20 != Y10 ))| ~ r2(X7,Y10) ) )),
% 0.23/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.48 fof(f12,conjecture,(
% 0.23/0.48 (! [Y1] :( (! [Y2] :( (! [Y3] :( ~ r1(Y3)| ~ r3(Y3,Y2,Y1) ))| (! [Y4] :( ~ r1(Y4)| ~ r2(Y4,Y2) ) )))| (! [Y5] :( Y1 != Y5| ~ r1(Y5) ) )) )),
% 0.23/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/0.48 fof(f13,negated_conjecture,(
% 0.23/0.48 ~((! [Y1] :( (! [Y2] :( (! [Y3] :( ~ r1(Y3)| ~ r3(Y3,Y2,Y1) ))| (! [Y4] :( ~ r1(Y4)| ~ r2(Y4,Y2) ) )))| (! [Y5] :( Y1 != Y5| ~ r1(Y5) ) )) ))),
% 0.23/0.48 inference(negated_conjecture,[status(cth)],[f12])).
% 0.23/0.48 fof(f14,definition,(
% 0.23/0.48 ![Y24,X19]: (sP0_prd(X19,Y24)<=>(~r1(X19)&~X19=Y24))),
% 0.23/0.48 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.23/0.48 fof(f15,plain,(
% 0.23/0.48 ?[Y24]: ![X19]: (sP0_prd(X19,Y24)|(r1(X19)&X19=Y24))),
% 0.23/0.48 inference(formula_renaming,[status(thm)],[f1,f14])).
% 0.23/0.48 fof(f16,plain,(
% 0.23/0.48 ![X19]: (sP0_prd(X19,sK0_skl)|(r1(X19)&X19=sK0_skl))),
% 0.23/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y24,sK0_skl)],[f15])).
% 0.23/0.48 fof(f17,plain,(
% 0.23/0.48 ![X0]: (sP0_prd(X0,sK0_skl)|r1(X0))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f16])).
% 0.23/0.48 fof(f18,plain,(
% 0.23/0.48 ![X0]: (sP0_prd(X0,sK0_skl)|X0=sK0_skl)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f16])).
% 0.23/0.48 fof(f19,definition,(
% 0.23/0.48 ![X11,Y21,X12]: (sP1_prd(X12,Y21,X11)<=>(~r2(X11,X12)&~X12=Y21))),
% 0.23/0.48 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.23/0.48 fof(f20,plain,(
% 0.23/0.48 ![X11]: ?[Y21]: ![X12]: (sP1_prd(X12,Y21,X11)|(r2(X11,X12)&X12=Y21))),
% 0.23/0.48 inference(formula_renaming,[status(thm)],[f2,f19])).
% 0.23/0.48 fof(f21,plain,(
% 0.23/0.48 ![X11]: ![X12]: (sP1_prd(X12,sK1_skl(X11),X11)|(r2(X11,X12)&X12=sK1_skl(X11)))),
% 0.23/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y21,sK1_skl(X11))],[f20])).
% 0.23/0.48 fof(f23,plain,(
% 0.23/0.48 ![X0,X1]: (sP1_prd(X0,sK1_skl(X1),X1)|X0=sK1_skl(X1))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f21])).
% 0.23/0.48 fof(f24,definition,(
% 0.23/0.48 ![X13,X14,Y22,X15]: (sP2_prd(X15,Y22,X14,X13)<=>(~r3(X13,X14,X15)&~X15=Y22))),
% 0.23/0.48 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.23/0.48 fof(f25,plain,(
% 0.23/0.48 ![X13,X14]: ?[Y22]: ![X15]: (sP2_prd(X15,Y22,X14,X13)|(r3(X13,X14,X15)&X15=Y22))),
% 0.23/0.48 inference(formula_renaming,[status(thm)],[f3,f24])).
% 0.23/0.48 fof(f26,plain,(
% 0.23/0.48 ![X13,X14]: ![X15]: (sP2_prd(X15,sK2_skl(X14,X13),X14,X13)|(r3(X13,X14,X15)&X15=sK2_skl(X14,X13)))),
% 0.23/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y22,sK2_skl(X14,X13))],[f25])).
% 0.23/0.48 fof(f28,plain,(
% 0.23/0.48 ![X0,X1,X2]: (sP2_prd(X0,sK2_skl(X1,X2),X1,X2)|X0=sK2_skl(X1,X2))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f26])).
% 0.23/0.48 fof(f34,plain,(
% 0.23/0.48 ![X1,X8]: (((r2(X8,sK6_skl(X8,X1))&r3(X1,sK6_skl(X8,X1),sK5_skl(X8,X1)))&sK5_skl(X8,X1)=sK4_skl(X8,X1))&(r2(sK7_skl(X8,X1),sK4_skl(X8,X1))&r3(X1,X8,sK7_skl(X8,X1))))),
% 0.23/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl]),skolemize(Y4,sK4_skl(X8,X1)),skolemize(Y5,sK5_skl(X8,X1)),skolemize(Y15,sK6_skl(X8,X1)),skolemize(Y7,sK7_skl(X8,X1))],[f5])).
% 0.23/0.48 fof(f35,plain,(
% 0.23/0.48 ![X0,X1]: (r2(X0,sK6_skl(X0,X1)))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f34])).
% 0.23/0.48 fof(f36,plain,(
% 0.23/0.48 ![X0,X1]: (r3(X0,sK6_skl(X1,X0),sK5_skl(X1,X0)))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f34])).
% 0.23/0.48 fof(f37,plain,(
% 0.23/0.48 ![X0,X1]: (sK5_skl(X0,X1)=sK4_skl(X0,X1))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f34])).
% 0.23/0.48 fof(f38,plain,(
% 0.23/0.48 ![X0,X1]: (r2(sK7_skl(X0,X1),sK4_skl(X0,X1)))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f34])).
% 0.23/0.48 fof(f62,plain,(
% 0.23/0.48 ![Y10]: ((![Y20]: (~r1(Y20)|~Y20=Y10))|(![X7]: ~r2(X7,Y10)))),
% 0.23/0.48 inference(miniscoping,[status(thm)],[f11])).
% 0.23/0.48 fof(f63,plain,(
% 0.23/0.48 ![X0,X1,X2]: (~r1(X0)|~X0=X1|~r2(X2,X1))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f62])).
% 0.23/0.48 fof(f64,plain,(
% 0.23/0.48 (?[Y1]: ((?[Y2]: ((?[Y3]: (r1(Y3)&r3(Y3,Y2,Y1)))&(?[Y4]: (r1(Y4)&r2(Y4,Y2)))))&(?[Y5]: (Y1=Y5&r1(Y5)))))),
% 0.23/0.48 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.23/0.48 fof(f65,plain,(
% 0.23/0.48 (((r1(sK22_skl)&r3(sK22_skl,sK21_skl,sK20_skl))&(r1(sK23_skl)&r2(sK23_skl,sK21_skl)))&(sK20_skl=sK24_skl&r1(sK24_skl)))),
% 0.23/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(Y1,sK20_skl),skolemize(Y2,sK21_skl),skolemize(Y3,sK22_skl),skolemize(Y4,sK23_skl),skolemize(Y5,sK24_skl)],[f64])).
% 0.23/0.48 fof(f66,plain,(
% 0.23/0.48 r1(sK22_skl)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f65])).
% 0.23/0.48 fof(f67,plain,(
% 0.23/0.48 r3(sK22_skl,sK21_skl,sK20_skl)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f65])).
% 0.23/0.48 fof(f68,plain,(
% 0.23/0.48 r1(sK23_skl)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f65])).
% 0.23/0.48 fof(f69,plain,(
% 0.23/0.48 r2(sK23_skl,sK21_skl)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f65])).
% 0.23/0.48 fof(f70,plain,(
% 0.23/0.48 sK20_skl=sK24_skl),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f65])).
% 0.23/0.48 fof(f71,plain,(
% 0.23/0.48 r1(sK24_skl)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f65])).
% 0.23/0.48 fof(f72,plain,(
% 0.23/0.48 ![Y24,X19]: ((~sP0_prd(X19,Y24)|(~r1(X19)&~X19=Y24))&(sP0_prd(X19,Y24)|(r1(X19)|X19=Y24)))),
% 0.23/0.48 inference(NNF_transformation,[status(thm)],[f14])).
% 0.23/0.48 fof(f73,plain,(
% 0.23/0.48 (![Y24,X19]: (~sP0_prd(X19,Y24)|(~r1(X19)&~X19=Y24)))&(![Y24,X19]: (sP0_prd(X19,Y24)|(r1(X19)|X19=Y24)))),
% 0.23/0.48 inference(miniscoping,[status(thm)],[f72])).
% 0.23/0.48 fof(f74,plain,(
% 0.23/0.48 ![X0,X1]: (~sP0_prd(X0,X1)|~r1(X0))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f73])).
% 0.23/0.48 fof(f75,plain,(
% 0.23/0.48 ![X0,X1]: (~sP0_prd(X0,X1)|~X0=X1)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f73])).
% 0.23/0.48 fof(f77,plain,(
% 0.23/0.48 ![X11,Y21,X12]: ((~sP1_prd(X12,Y21,X11)|(~r2(X11,X12)&~X12=Y21))&(sP1_prd(X12,Y21,X11)|(r2(X11,X12)|X12=Y21)))),
% 0.23/0.48 inference(NNF_transformation,[status(thm)],[f19])).
% 0.23/0.48 fof(f78,plain,(
% 0.23/0.48 (![X11,Y21,X12]: (~sP1_prd(X12,Y21,X11)|(~r2(X11,X12)&~X12=Y21)))&(![X11,Y21,X12]: (sP1_prd(X12,Y21,X11)|(r2(X11,X12)|X12=Y21)))),
% 0.23/0.48 inference(miniscoping,[status(thm)],[f77])).
% 0.23/0.48 fof(f79,plain,(
% 0.23/0.48 ![X0,X1,X2]: (~sP1_prd(X0,X1,X2)|~r2(X2,X0))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f78])).
% 0.23/0.48 fof(f82,plain,(
% 0.23/0.48 ![X13,X14,Y22,X15]: ((~sP2_prd(X15,Y22,X14,X13)|(~r3(X13,X14,X15)&~X15=Y22))&(sP2_prd(X15,Y22,X14,X13)|(r3(X13,X14,X15)|X15=Y22)))),
% 0.23/0.48 inference(NNF_transformation,[status(thm)],[f24])).
% 0.23/0.48 fof(f83,plain,(
% 0.23/0.48 (![X13,X14,Y22,X15]: (~sP2_prd(X15,Y22,X14,X13)|(~r3(X13,X14,X15)&~X15=Y22)))&(![X13,X14,Y22,X15]: (sP2_prd(X15,Y22,X14,X13)|(r3(X13,X14,X15)|X15=Y22)))),
% 0.23/0.48 inference(miniscoping,[status(thm)],[f82])).
% 0.23/0.48 fof(f84,plain,(
% 0.23/0.48 ![X0,X1,X2,X3]: (~sP2_prd(X0,X1,X2,X3)|~r3(X3,X2,X0))),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f83])).
% 0.23/0.48 fof(f98,plain,(
% 0.23/0.48 ![X0,X1]: (~r1(X0)|~r2(X1,X0))),
% 0.23/0.48 inference(destructive_equality_resolution,[status(thm)],[f63])).
% 0.23/0.48 fof(f99,plain,(
% 0.23/0.48 ![X0]: (~sP0_prd(X0,X0))),
% 0.23/0.48 inference(destructive_equality_resolution,[status(thm)],[f75])).
% 0.23/0.48 fof(f104,plain,(
% 0.23/0.48 r1(sK20_skl)),
% 0.23/0.48 inference(forward_demodulation,[status(thm)],[f70,f71])).
% 0.23/0.48 fof(f107,plain,(
% 0.23/0.48 r1(sK0_skl)),
% 0.23/0.48 inference(resolution,[status(thm)],[f17,f99])).
% 0.23/0.48 fof(f116,plain,(
% 0.23/0.48 ![X0,X1]: (r3(X0,sK6_skl(X1,X0),sK4_skl(X1,X0)))),
% 0.23/0.48 inference(backward_demodulation,[status(thm)],[f37,f36])).
% 0.23/0.48 fof(f117,plain,(
% 0.23/0.48 ![X0,X1]: (~r1(sK4_skl(X0,X1)))),
% 0.23/0.48 inference(resolution,[status(thm)],[f38,f98])).
% 0.23/0.48 fof(f132,plain,(
% 0.23/0.48 ![X0]: (~r1(X0)|X0=sK0_skl)),
% 0.23/0.48 inference(resolution,[status(thm)],[f74,f18])).
% 0.23/0.48 fof(f136,plain,(
% 0.23/0.48 ![X0,X1]: (~r2(X0,X1)|X1=sK1_skl(X0))),
% 0.23/0.48 inference(resolution,[status(thm)],[f79,f23])).
% 0.23/0.48 fof(f145,plain,(
% 0.23/0.48 ![X0,X1,X2]: (~r3(X0,X1,X2)|X2=sK2_skl(X1,X0))),
% 0.23/0.48 inference(resolution,[status(thm)],[f84,f28])).
% 0.23/0.48 fof(f155,plain,(
% 0.23/0.48 sK20_skl=sK0_skl),
% 0.23/0.48 inference(resolution,[status(thm)],[f132,f104])).
% 0.23/0.48 fof(f156,plain,(
% 0.23/0.48 sK23_skl=sK0_skl),
% 0.23/0.48 inference(resolution,[status(thm)],[f132,f68])).
% 0.23/0.48 fof(f157,plain,(
% 0.23/0.48 sK22_skl=sK0_skl),
% 0.23/0.48 inference(resolution,[status(thm)],[f132,f66])).
% 0.23/0.48 fof(f160,plain,(
% 0.23/0.48 r3(sK22_skl,sK21_skl,sK0_skl)),
% 0.23/0.48 inference(backward_demodulation,[status(thm)],[f155,f67])).
% 0.23/0.48 fof(f162,plain,(
% 0.23/0.48 r2(sK0_skl,sK21_skl)),
% 0.23/0.48 inference(backward_demodulation,[status(thm)],[f156,f69])).
% 0.23/0.48 fof(f171,plain,(
% 0.23/0.48 r3(sK0_skl,sK21_skl,sK0_skl)),
% 0.23/0.48 inference(forward_demodulation,[status(thm)],[f157,f160])).
% 0.23/0.48 fof(f192,plain,(
% 0.23/0.48 sK21_skl=sK1_skl(sK0_skl)),
% 0.23/0.48 inference(resolution,[status(thm)],[f136,f162])).
% 0.23/0.48 fof(f197,plain,(
% 0.23/0.48 ![X0,X1]: (sK6_skl(X0,X1)=sK1_skl(X0))),
% 0.23/0.48 inference(resolution,[status(thm)],[f136,f35])).
% 0.23/0.48 fof(f198,plain,(
% 0.23/0.48 sK0_skl=sK2_skl(sK21_skl,sK0_skl)),
% 0.23/0.48 inference(resolution,[status(thm)],[f145,f171])).
% 0.23/0.48 fof(f216,plain,(
% 0.23/0.48 ![X0]: (sP2_prd(X0,sK0_skl,sK21_skl,sK0_skl)|X0=sK2_skl(sK21_skl,sK0_skl))),
% 0.23/0.48 inference(paramodulation,[status(thm)],[f198,f28])).
% 0.23/0.48 fof(f218,plain,(
% 0.23/0.48 ![X0]: (sP2_prd(X0,sK0_skl,sK21_skl,sK0_skl)|X0=sK0_skl)),
% 0.23/0.48 inference(forward_demodulation,[status(thm)],[f198,f216])).
% 0.23/0.48 fof(f235,plain,(
% 0.23/0.48 ![X0]: (X0=sK0_skl|~r3(sK0_skl,sK21_skl,X0))),
% 0.23/0.48 inference(resolution,[status(thm)],[f218,f84])).
% 0.23/0.48 fof(f245,plain,(
% 0.23/0.48 ![X0,X1]: (r3(X0,sK1_skl(X1),sK4_skl(X1,X0)))),
% 0.23/0.48 inference(backward_demodulation,[status(thm)],[f197,f116])).
% 0.23/0.48 fof(f252,plain,(
% 0.23/0.48 ![X0]: (r3(X0,sK21_skl,sK4_skl(sK0_skl,X0)))),
% 0.23/0.48 inference(paramodulation,[status(thm)],[f192,f245])).
% 0.23/0.48 fof(f274,plain,(
% 0.23/0.48 sK4_skl(sK0_skl,sK0_skl)=sK0_skl),
% 0.23/0.48 inference(resolution,[status(thm)],[f252,f235])).
% 0.23/0.48 fof(f314,plain,(
% 0.23/0.48 ~r1(sK0_skl)),
% 0.23/0.48 inference(paramodulation,[status(thm)],[f274,f117])).
% 0.23/0.48 fof(f318,plain,(
% 0.23/0.48 $false),
% 0.23/0.48 inference(forward_subsumption_resolution,[status(thm)],[f314,f107])).
% 0.23/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.51 % Elapsed time: 0.070279 seconds
% 0.23/0.51 % CPU time: 0.168037 seconds
% 0.23/0.51 % Total memory used: 70.852 MB
% 0.23/0.51 % Net memory used: 70.771 MB
%------------------------------------------------------------------------------