%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUN076+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:26 PM UTC 2026
% Result : Theorem 2.55s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUN076+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n010.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 03:24:56 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 2.55/0.84 % Refutation found
% 2.55/0.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.55/0.84 % SZS output start CNFRefutation for theBenchmark
% 2.55/0.84 fof(f1,axiom,(
% 2.55/0.84 (? [Y24] :(! [X19] :( ( id(X19,Y24)& r1(X19) )| ( ~ r1(X19)& ~ id(X19,Y24) ) ) ))),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f2,axiom,(
% 2.55/0.84 (! [X11] :(? [Y21] :(! [X12] :( ( id(X12,Y21)& r2(X11,X12) )| ( ~ r2(X11,X12)& ~ id(X12,Y21) ) ) )))),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f5,axiom,(
% 2.55/0.84 (! [X20] : id(X20,X20) )),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f6,axiom,(
% 2.55/0.84 (! [X21,X22] :( ~ id(X21,X22)| id(X22,X21) ) )),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f7,axiom,(
% 2.55/0.84 (! [X23,X24,X25] :( ~ id(X23,X24)| id(X23,X25)| ~ id(X24,X25) ) )),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f8,axiom,(
% 2.55/0.84 (! [X26,X27] :( ~ id(X26,X27)| ( ~ r1(X26)& ~ r1(X27) )| ( r1(X26)& r1(X27) ) ) )),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f15,axiom,(
% 2.55/0.84 (! [X4] :(? [Y9] :( id(Y9,X4)& (? [Y16] :( r1(Y16)& r3(X4,Y16,Y9) ) )) ))),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f16,axiom,(
% 2.55/0.84 (! [X5] :(? [Y8] :( (? [Y17] :( r1(Y17)& r4(X5,Y17,Y8) ))& (? [Y18] :( id(Y8,Y18)& r1(Y18) ) )) ))),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f19,conjecture,(
% 2.55/0.84 (? [Y1,Y2,Y3] :( (? [Y4] :( id(Y4,Y1)& (? [Y6] :( r4(Y6,Y2,Y4)& (? [Y7] :( r2(Y7,Y6)& (? [Y8] :( r1(Y8)& r2(Y8,Y7) ) )) )) )))& (? [Y5] :( id(Y5,Y1)& r3(Y2,Y3,Y5) ) )) )),
% 2.55/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.55/0.84 fof(f20,negated_conjecture,(
% 2.55/0.84 ~((? [Y1,Y2,Y3] :( (? [Y4] :( id(Y4,Y1)& (? [Y6] :( r4(Y6,Y2,Y4)& (? [Y7] :( r2(Y7,Y6)& (? [Y8] :( r1(Y8)& r2(Y8,Y7) ) )) )) )))& (? [Y5] :( id(Y5,Y1)& r3(Y2,Y3,Y5) ) )) ))),
% 2.55/0.84 inference(negated_conjecture,[status(cth)],[f19])).
% 2.55/0.84 fof(f21,definition,(
% 2.55/0.84 ![Y24,X19]: (sP0_prd(X19,Y24)<=>(id(X19,Y24)&r1(X19)))),
% 2.55/0.84 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 2.55/0.84 fof(f22,plain,(
% 2.55/0.84 ?[Y24]: ![X19]: (sP0_prd(X19,Y24)|(~r1(X19)&~id(X19,Y24)))),
% 2.55/0.84 inference(formula_renaming,[status(thm)],[f1,f21])).
% 2.55/0.84 fof(f23,plain,(
% 2.55/0.84 ![X19]: (sP0_prd(X19,sK0_skl)|(~r1(X19)&~id(X19,sK0_skl)))),
% 2.55/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y24,sK0_skl)],[f22])).
% 2.55/0.84 fof(f24,plain,(
% 2.55/0.84 ![X0]: (sP0_prd(X0,sK0_skl)|~r1(X0))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f23])).
% 2.55/0.84 fof(f26,definition,(
% 2.55/0.84 ![X11,Y21,X12]: (sP1_prd(X12,Y21,X11)<=>(id(X12,Y21)&r2(X11,X12)))),
% 2.55/0.84 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 2.55/0.84 fof(f27,plain,(
% 2.55/0.84 ![X11]: ?[Y21]: ![X12]: (sP1_prd(X12,Y21,X11)|(~r2(X11,X12)&~id(X12,Y21)))),
% 2.55/0.84 inference(formula_renaming,[status(thm)],[f2,f26])).
% 2.55/0.84 fof(f28,plain,(
% 2.55/0.84 ![X11]: ![X12]: (sP1_prd(X12,sK1_skl(X11),X11)|(~r2(X11,X12)&~id(X12,sK1_skl(X11))))),
% 2.55/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y21,sK1_skl(X11))],[f27])).
% 2.55/0.84 fof(f30,plain,(
% 2.55/0.84 ![X0,X1]: (sP1_prd(X0,sK1_skl(X1),X1)|~id(X0,sK1_skl(X1)))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f28])).
% 2.55/0.84 fof(f41,plain,(
% 2.55/0.84 ![X0]: (id(X0,X0))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f5])).
% 2.55/0.84 fof(f42,plain,(
% 2.55/0.84 ![X0,X1]: (~id(X0,X1)|id(X1,X0))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f6])).
% 2.55/0.84 fof(f43,plain,(
% 2.55/0.84 ![X24,X25]: ((![X23]: (~id(X23,X24)|id(X23,X25)))|~id(X24,X25))),
% 2.55/0.84 inference(miniscoping,[status(thm)],[f7])).
% 2.55/0.84 fof(f44,plain,(
% 2.55/0.84 ![X0,X1,X2]: (~id(X0,X1)|id(X0,X2)|~id(X1,X2))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f43])).
% 2.55/0.84 fof(f45,definition,(
% 2.55/0.84 ![X26,X27]: (sP4_prd(X27,X26)<=>(~r1(X26)&~r1(X27)))),
% 2.55/0.84 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 2.55/0.84 fof(f46,plain,(
% 2.55/0.84 ![X26,X27]: ((~id(X26,X27)|sP4_prd(X27,X26))|(r1(X26)&r1(X27)))),
% 2.55/0.84 inference(formula_renaming,[status(thm)],[f8,f45])).
% 2.55/0.84 fof(f47,plain,(
% 2.55/0.84 ![X0,X1]: (~id(X0,X1)|sP4_prd(X1,X0)|r1(X0))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f46])).
% 2.55/0.84 fof(f74,plain,(
% 2.55/0.84 ![X4]: (id(sK12_skl(X4),X4)&(r1(sK13_skl(X4))&r3(X4,sK13_skl(X4),sK12_skl(X4))))),
% 2.55/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(Y9,sK12_skl(X4)),skolemize(Y16,sK13_skl(X4))],[f15])).
% 2.55/0.84 fof(f75,plain,(
% 2.55/0.84 ![X0]: (id(sK12_skl(X0),X0))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f74])).
% 2.55/0.84 fof(f77,plain,(
% 2.55/0.84 ![X0]: (r3(X0,sK13_skl(X0),sK12_skl(X0)))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f74])).
% 2.55/0.84 fof(f78,plain,(
% 2.55/0.84 ![X5]: ((r1(sK15_skl(X5))&r4(X5,sK15_skl(X5),sK14_skl(X5)))&(id(sK14_skl(X5),sK16_skl(X5))&r1(sK16_skl(X5))))),
% 2.55/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(Y8,sK14_skl(X5)),skolemize(Y17,sK15_skl(X5)),skolemize(Y18,sK16_skl(X5))],[f16])).
% 2.55/0.84 fof(f79,plain,(
% 2.55/0.84 ![X0]: (r1(sK15_skl(X0)))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f78])).
% 2.55/0.84 fof(f80,plain,(
% 2.55/0.84 ![X0]: (r4(X0,sK15_skl(X0),sK14_skl(X0)))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f78])).
% 2.55/0.84 fof(f81,plain,(
% 2.55/0.84 ![X0]: (id(sK14_skl(X0),sK16_skl(X0)))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f78])).
% 2.55/0.84 fof(f82,plain,(
% 2.55/0.84 ![X0]: (r1(sK16_skl(X0)))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f78])).
% 2.55/0.84 fof(f91,plain,(
% 2.55/0.84 (![Y1,Y2,Y3]: ((![Y4]: (~id(Y4,Y1)|(![Y6]: (~r4(Y6,Y2,Y4)|(![Y7]: (~r2(Y7,Y6)|(![Y8]: (~r1(Y8)|~r2(Y8,Y7)))))))))|(![Y5]: (~id(Y5,Y1)|~r3(Y2,Y3,Y5)))))),
% 2.55/0.84 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 2.55/0.84 fof(f92,plain,(
% 2.55/0.84 ![Y1,Y2]: ((![Y4]: (~id(Y4,Y1)|(![Y6]: (~r4(Y6,Y2,Y4)|(![Y7]: (~r2(Y7,Y6)|(![Y8]: (~r1(Y8)|~r2(Y8,Y7)))))))))|(![Y5]: (~id(Y5,Y1)|(![Y3]: ~r3(Y2,Y3,Y5)))))),
% 2.55/0.84 inference(miniscoping,[status(thm)],[f91])).
% 2.55/0.84 fof(f93,plain,(
% 2.55/0.84 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~id(X0,X1)|~r4(X2,X3,X0)|~r2(X4,X2)|~r1(X5)|~r2(X5,X4)|~id(X6,X1)|~r3(X3,X7,X6))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f92])).
% 2.55/0.84 fof(f94,plain,(
% 2.55/0.84 ![Y24,X19]: ((~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19)))&(sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 2.55/0.84 inference(NNF_transformation,[status(thm)],[f21])).
% 2.55/0.84 fof(f95,plain,(
% 2.55/0.84 (![Y24,X19]: (~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19))))&(![Y24,X19]: (sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 2.55/0.84 inference(miniscoping,[status(thm)],[f94])).
% 2.55/0.84 fof(f96,plain,(
% 2.55/0.84 ![X0,X1]: (~sP0_prd(X0,X1)|id(X0,X1))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f95])).
% 2.55/0.84 fof(f99,plain,(
% 2.55/0.84 ![X11,Y21,X12]: ((~sP1_prd(X12,Y21,X11)|(id(X12,Y21)&r2(X11,X12)))&(sP1_prd(X12,Y21,X11)|(~id(X12,Y21)|~r2(X11,X12))))),
% 2.55/0.84 inference(NNF_transformation,[status(thm)],[f26])).
% 2.55/0.84 fof(f100,plain,(
% 2.55/0.84 (![X11,Y21,X12]: (~sP1_prd(X12,Y21,X11)|(id(X12,Y21)&r2(X11,X12))))&(![X11,Y21,X12]: (sP1_prd(X12,Y21,X11)|(~id(X12,Y21)|~r2(X11,X12))))),
% 2.55/0.84 inference(miniscoping,[status(thm)],[f99])).
% 2.55/0.84 fof(f102,plain,(
% 2.55/0.84 ![X0,X1,X2]: (~sP1_prd(X0,X1,X2)|r2(X2,X0))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f100])).
% 2.55/0.84 fof(f114,plain,(
% 2.55/0.84 ![X26,X27]: ((~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27)))&(sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 2.55/0.84 inference(NNF_transformation,[status(thm)],[f45])).
% 2.55/0.84 fof(f115,plain,(
% 2.55/0.84 (![X26,X27]: (~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27))))&(![X26,X27]: (sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 2.55/0.84 inference(miniscoping,[status(thm)],[f114])).
% 2.55/0.84 fof(f117,plain,(
% 2.55/0.84 ![X0,X1]: (~sP4_prd(X0,X1)|~r1(X0))),
% 2.55/0.84 inference(cnf_transformation,[status(thm)],[f115])).
% 2.55/0.84 fof(f144,plain,(
% 2.55/0.84 ![X0]: (sP0_prd(sK15_skl(X0),sK0_skl))),
% 2.55/0.84 inference(resolution,[status(thm)],[f79,f24])).
% 2.55/0.84 fof(f148,plain,(
% 2.55/0.84 ![X0]: (id(X0,sK12_skl(X0)))),
% 2.55/0.84 inference(resolution,[status(thm)],[f75,f42])).
% 2.55/0.84 fof(f149,plain,(
% 2.55/0.84 ![X0,X1]: (~id(X0,X1)|id(X0,sK12_skl(X1)))),
% 2.55/0.84 inference(resolution,[status(thm)],[f148,f44])).
% 2.55/0.84 fof(f157,plain,(
% 2.55/0.84 ![X0]: (sP1_prd(sK12_skl(sK1_skl(X0)),sK1_skl(X0),X0))),
% 2.55/0.84 inference(resolution,[status(thm)],[f30,f75])).
% 2.55/0.84 fof(f158,plain,(
% 2.55/0.84 ![X0]: (sP1_prd(sK1_skl(X0),sK1_skl(X0),X0))),
% 2.55/0.84 inference(resolution,[status(thm)],[f30,f41])).
% 2.55/0.84 fof(f274,plain,(
% 2.55/0.84 ![X0]: (sP4_prd(sK16_skl(X0),sK14_skl(X0))|r1(sK14_skl(X0)))),
% 2.55/0.84 inference(resolution,[status(thm)],[f81,f47])).
% 2.55/0.84 fof(f279,plain,(
% 2.55/0.84 ![X0]: (id(sK15_skl(X0),sK0_skl))),
% 2.55/0.84 inference(resolution,[status(thm)],[f96,f144])).
% 2.55/0.84 fof(f298,plain,(
% 2.55/0.84 ![X0]: (id(sK0_skl,sK15_skl(X0)))),
% 2.55/0.84 inference(resolution,[status(thm)],[f279,f42])).
% 2.55/0.84 fof(f354,plain,(
% 2.55/0.84 ![X0]: (id(sK0_skl,sK12_skl(sK15_skl(X0))))),
% 2.55/0.84 inference(resolution,[status(thm)],[f298,f149])).
% 2.55/0.84 fof(f386,plain,(
% 2.55/0.84 ![X0,X1,X2,X3,X4,X5]: (~id(sK14_skl(X0),X1)|~r2(X2,X0)|~r1(X3)|~r2(X3,X2)|~id(X4,X1)|~r3(sK15_skl(X0),X5,X4))),
% 2.55/0.84 inference(resolution,[status(thm)],[f80,f93])).
% 2.55/0.84 fof(f388,plain,(
% 2.55/0.84 ![X0]: (r2(X0,sK1_skl(X0)))),
% 2.55/0.84 inference(resolution,[status(thm)],[f102,f158])).
% 2.55/0.84 fof(f429,plain,(
% 2.55/0.84 ![X0,X1,X2,X3]: (~id(sK14_skl(X0),X1)|~r2(X2,X0)|~r1(X3)|~r2(X3,X2)|~id(sK12_skl(sK15_skl(X0)),X1))),
% 2.55/0.84 inference(resolution,[status(thm)],[f386,f77])).
% 2.55/0.84 fof(f543,plain,(
% 2.55/0.84 ![X0]: (id(sK12_skl(sK15_skl(X0)),sK0_skl))),
% 2.55/0.84 inference(resolution,[status(thm)],[f354,f42])).
% 2.55/0.84 fof(f698,plain,(
% 2.55/0.84 ![X0,X1,X2]: (~id(sK14_skl(X0),sK0_skl)|~r2(X1,X0)|~r1(X2)|~r2(X2,X1))),
% 2.55/0.84 inference(resolution,[status(thm)],[f543,f429])).
% 2.55/0.84 fof(f1271,plain,(
% 2.55/0.84 ![X0]: (r2(X0,sK12_skl(sK1_skl(X0))))),
% 2.55/0.84 inference(resolution,[status(thm)],[f157,f102])).
% 2.55/0.84 fof(f1426,plain,(
% 2.55/0.84 ![X0]: (r1(sK14_skl(X0))|~r1(sK16_skl(X0)))),
% 2.55/0.84 inference(resolution,[status(thm)],[f274,f117])).
% 2.55/0.84 fof(f1428,plain,(
% 2.55/0.84 ![X0]: (r1(sK14_skl(X0)))),
% 2.55/0.84 inference(forward_subsumption_resolution,[status(thm)],[f1426,f82])).
% 2.55/0.84 fof(f1452,plain,(
% 2.55/0.84 ![X0]: (sP0_prd(sK14_skl(X0),sK0_skl))),
% 2.55/0.84 inference(resolution,[status(thm)],[f1428,f24])).
% 2.55/0.84 fof(f1460,plain,(
% 2.55/0.84 ![X0]: (id(sK14_skl(X0),sK0_skl))),
% 2.55/0.84 inference(resolution,[status(thm)],[f1452,f96])).
% 2.55/0.84 fof(f1462,plain,(
% 2.55/0.84 ![X0,X1,X2]: (~r2(X0,X1)|~r1(X2)|~r2(X2,X0))),
% 2.55/0.84 inference(backward_subsumption_resolution,[status(thm)],[f698,f1460])).
% 2.55/0.84 fof(f1635,plain,(
% 2.55/0.84 ![X0,X1]: (~r2(sK1_skl(X0),X1)|~r1(X0))),
% 2.55/0.84 inference(resolution,[status(thm)],[f1462,f388])).
% 2.55/0.84 fof(f1638,plain,(
% 2.55/0.84 ![X0]: (~r1(X0))),
% 2.55/0.84 inference(resolution,[status(thm)],[f1635,f1271])).
% 2.55/0.84 fof(f1652,plain,(
% 2.55/0.84 $false),
% 2.55/0.84 inference(backward_subsumption_resolution,[status(thm)],[f1428,f1638])).
% 2.55/0.84 % SZS output end CNFRefutation for theBenchmark.p
% 2.55/0.88 % Elapsed time: 0.416981 seconds
% 2.55/0.88 % CPU time: 2.918186 seconds
% 2.55/0.88 % Total memory used: 40.393 MB
% 2.55/0.88 % Net memory used: 35.743 MB
%------------------------------------------------------------------------------