%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUN059+1 : TPTP v9.3.1. Bugfixed v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:24 PM UTC 2026
% Result : Theorem 48.47s 6.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN059+1 : TPTP v9.3.1. Bugfixed v7.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n008.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 03:24:23 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.03/0.37 % Drodi V4.1.1
% 48.47/6.69 % Refutation found
% 48.47/6.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 48.47/6.69 % SZS output start CNFRefutation for theBenchmark
% 48.47/6.69 fof(f1,axiom,(
% 48.47/6.69 (? [Y24] :(! [X19] :( ( id(X19,Y24)& r1(X19) )| ( ~ r1(X19)& ~ id(X19,Y24) ) ) ))),
% 48.47/6.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.69 fof(f3,axiom,(
% 48.47/6.69 (! [X13,X14] :(? [Y22] :(! [X15] :( ( id(X15,Y22)& r3(X13,X14,X15) )| ( ~ r3(X13,X14,X15)& ~ id(X15,Y22) ) ) )))),
% 48.47/6.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.69 fof(f4,axiom,(
% 48.47/6.69 (! [X16,X17] :(? [Y23] :(! [X18] :( ( id(X18,Y23)& r4(X16,X17,X18) )| ( ~ r4(X16,X17,X18)& ~ id(X18,Y23) ) ) )))),
% 48.47/6.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.69 fof(f6,axiom,(
% 48.47/6.69 (! [X21,X22] :( ~ id(X21,X22)| id(X22,X21) ) )),
% 48.47/6.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.69 fof(f7,axiom,(
% 48.47/6.69 (! [X23,X24,X25] :( ~ id(X23,X24)| id(X23,X25)| ~ id(X24,X25) ) )),
% 48.47/6.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.69 fof(f8,axiom,(
% 48.47/6.69 (! [X26,X27] :( ~ id(X26,X27)| ( ~ r1(X26)& ~ r1(X27) )| ( r1(X26)& r1(X27) ) ) )),
% 48.47/6.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.70 fof(f11,axiom,(
% 48.47/6.70 (! [X38,X39,X40,X41,X42,X43] :( ~ id(X38,X41)| ~ id(X39,X42)| ~ id(X40,X43)| ( ~ r4(X38,X39,X40)& ~ r4(X41,X42,X43) )| ( r4(X38,X39,X40)& r4(X41,X42,X43) ) ) )),
% 48.47/6.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.70 fof(f15,axiom,(
% 48.47/6.70 (! [X4] :(? [Y9] :( id(Y9,X4)& (? [Y16] :( r1(Y16)& r3(X4,Y16,Y9) ) )) ))),
% 48.47/6.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.70 fof(f16,axiom,(
% 48.47/6.70 (! [X5] :(? [Y8] :( (? [Y17] :( r1(Y17)& r4(X5,Y17,Y8) ))& (? [Y18] :( id(Y8,Y18)& r1(Y18) ) )) ))),
% 48.47/6.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.70 fof(f19,conjecture,(
% 48.47/6.70 (? [Y1,Y3,Y2,Y4] :( (? [Y5] :( id(Y4,Y5)& r4(Y2,Y2,Y5) ))& (? [Y6] :( r4(Y3,Y3,Y6)& (? [Y7] :( r4(Y1,Y1,Y7)& r3(Y7,Y6,Y4) ) )) )) )),
% 48.47/6.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.47/6.70 fof(f20,negated_conjecture,(
% 48.47/6.70 ~((? [Y1,Y3,Y2,Y4] :( (? [Y5] :( id(Y4,Y5)& r4(Y2,Y2,Y5) ))& (? [Y6] :( r4(Y3,Y3,Y6)& (? [Y7] :( r4(Y1,Y1,Y7)& r3(Y7,Y6,Y4) ) )) )) ))),
% 48.47/6.70 inference(negated_conjecture,[status(cth)],[f19])).
% 48.47/6.70 fof(f21,definition,(
% 48.47/6.70 ![Y24,X19]: (sP0_prd(X19,Y24)<=>(id(X19,Y24)&r1(X19)))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 48.47/6.70 fof(f22,plain,(
% 48.47/6.70 ?[Y24]: ![X19]: (sP0_prd(X19,Y24)|(~r1(X19)&~id(X19,Y24)))),
% 48.47/6.70 inference(formula_renaming,[status(thm)],[f1,f21])).
% 48.47/6.70 fof(f23,plain,(
% 48.47/6.70 ![X19]: (sP0_prd(X19,sK0_skl)|(~r1(X19)&~id(X19,sK0_skl)))),
% 48.47/6.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y24,sK0_skl)],[f22])).
% 48.47/6.70 fof(f24,plain,(
% 48.47/6.70 ![X0]: (sP0_prd(X0,sK0_skl)|~r1(X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f23])).
% 48.47/6.70 fof(f25,plain,(
% 48.47/6.70 ![X0]: (sP0_prd(X0,sK0_skl)|~id(X0,sK0_skl))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f23])).
% 48.47/6.70 fof(f31,definition,(
% 48.47/6.70 ![X13,X14,Y22,X15]: (sP2_prd(X15,Y22,X14,X13)<=>(id(X15,Y22)&r3(X13,X14,X15)))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 48.47/6.70 fof(f32,plain,(
% 48.47/6.70 ![X13,X14]: ?[Y22]: ![X15]: (sP2_prd(X15,Y22,X14,X13)|(~r3(X13,X14,X15)&~id(X15,Y22)))),
% 48.47/6.70 inference(formula_renaming,[status(thm)],[f3,f31])).
% 48.47/6.70 fof(f33,plain,(
% 48.47/6.70 ![X13,X14]: ![X15]: (sP2_prd(X15,sK2_skl(X14,X13),X14,X13)|(~r3(X13,X14,X15)&~id(X15,sK2_skl(X14,X13))))),
% 48.47/6.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y22,sK2_skl(X14,X13))],[f32])).
% 48.47/6.70 fof(f34,plain,(
% 48.47/6.70 ![X0,X1,X2]: (sP2_prd(X0,sK2_skl(X1,X2),X1,X2)|~r3(X2,X1,X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f33])).
% 48.47/6.70 fof(f35,plain,(
% 48.47/6.70 ![X0,X1,X2]: (sP2_prd(X0,sK2_skl(X1,X2),X1,X2)|~id(X0,sK2_skl(X1,X2)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f33])).
% 48.47/6.70 fof(f36,definition,(
% 48.47/6.70 ![X16,X17,Y23,X18]: (sP3_prd(X18,Y23,X17,X16)<=>(id(X18,Y23)&r4(X16,X17,X18)))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 48.47/6.70 fof(f37,plain,(
% 48.47/6.70 ![X16,X17]: ?[Y23]: ![X18]: (sP3_prd(X18,Y23,X17,X16)|(~r4(X16,X17,X18)&~id(X18,Y23)))),
% 48.47/6.70 inference(formula_renaming,[status(thm)],[f4,f36])).
% 48.47/6.70 fof(f38,plain,(
% 48.47/6.70 ![X16,X17]: ![X18]: (sP3_prd(X18,sK3_skl(X17,X16),X17,X16)|(~r4(X16,X17,X18)&~id(X18,sK3_skl(X17,X16))))),
% 48.47/6.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Y23,sK3_skl(X17,X16))],[f37])).
% 48.47/6.70 fof(f39,plain,(
% 48.47/6.70 ![X0,X1,X2]: (sP3_prd(X0,sK3_skl(X1,X2),X1,X2)|~r4(X2,X1,X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f38])).
% 48.47/6.70 fof(f40,plain,(
% 48.47/6.70 ![X0,X1,X2]: (sP3_prd(X0,sK3_skl(X1,X2),X1,X2)|~id(X0,sK3_skl(X1,X2)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f38])).
% 48.47/6.70 fof(f42,plain,(
% 48.47/6.70 ![X0,X1]: (~id(X0,X1)|id(X1,X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f6])).
% 48.47/6.70 fof(f43,plain,(
% 48.47/6.70 ![X24,X25]: ((![X23]: (~id(X23,X24)|id(X23,X25)))|~id(X24,X25))),
% 48.47/6.70 inference(miniscoping,[status(thm)],[f7])).
% 48.47/6.70 fof(f44,plain,(
% 48.47/6.70 ![X0,X1,X2]: (~id(X0,X1)|id(X0,X2)|~id(X1,X2))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f43])).
% 48.47/6.70 fof(f45,definition,(
% 48.47/6.70 ![X26,X27]: (sP4_prd(X27,X26)<=>(~r1(X26)&~r1(X27)))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 48.47/6.70 fof(f46,plain,(
% 48.47/6.70 ![X26,X27]: ((~id(X26,X27)|sP4_prd(X27,X26))|(r1(X26)&r1(X27)))),
% 48.47/6.70 inference(formula_renaming,[status(thm)],[f8,f45])).
% 48.47/6.70 fof(f48,plain,(
% 48.47/6.70 ![X0,X1]: (~id(X0,X1)|sP4_prd(X1,X0)|r1(X1))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f46])).
% 48.47/6.70 fof(f57,definition,(
% 48.47/6.70 ![X38,X39,X40,X41,X42,X43]: (sP7_prd(X43,X42,X41,X40,X39,X38)<=>(~r4(X38,X39,X40)&~r4(X41,X42,X43)))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 48.47/6.70 fof(f58,plain,(
% 48.47/6.70 ![X38,X39,X40,X41,X42,X43]: ((((~id(X38,X41)|~id(X39,X42))|~id(X40,X43))|sP7_prd(X43,X42,X41,X40,X39,X38))|(r4(X38,X39,X40)&r4(X41,X42,X43)))),
% 48.47/6.70 inference(formula_renaming,[status(thm)],[f11,f57])).
% 48.47/6.70 fof(f60,plain,(
% 48.47/6.70 ![X0,X1,X2,X3,X4,X5]: (~id(X0,X1)|~id(X2,X3)|~id(X4,X5)|sP7_prd(X5,X3,X1,X4,X2,X0)|r4(X1,X3,X5))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f58])).
% 48.47/6.70 fof(f74,plain,(
% 48.47/6.70 ![X4]: (id(sK12_skl(X4),X4)&(r1(sK13_skl(X4))&r3(X4,sK13_skl(X4),sK12_skl(X4))))),
% 48.47/6.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(Y9,sK12_skl(X4)),skolemize(Y16,sK13_skl(X4))],[f15])).
% 48.47/6.70 fof(f75,plain,(
% 48.47/6.70 ![X0]: (id(sK12_skl(X0),X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f74])).
% 48.47/6.70 fof(f76,plain,(
% 48.47/6.70 ![X0]: (r1(sK13_skl(X0)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f74])).
% 48.47/6.70 fof(f77,plain,(
% 48.47/6.70 ![X0]: (r3(X0,sK13_skl(X0),sK12_skl(X0)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f74])).
% 48.47/6.70 fof(f78,plain,(
% 48.47/6.70 ![X5]: ((r1(sK15_skl(X5))&r4(X5,sK15_skl(X5),sK14_skl(X5)))&(id(sK14_skl(X5),sK16_skl(X5))&r1(sK16_skl(X5))))),
% 48.47/6.70 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])).
% 48.47/6.70 fof(f79,plain,(
% 48.47/6.70 ![X0]: (r1(sK15_skl(X0)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f78])).
% 48.47/6.70 fof(f80,plain,(
% 48.47/6.70 ![X0]: (r4(X0,sK15_skl(X0),sK14_skl(X0)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f78])).
% 48.47/6.70 fof(f81,plain,(
% 48.47/6.70 ![X0]: (id(sK14_skl(X0),sK16_skl(X0)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f78])).
% 48.47/6.70 fof(f82,plain,(
% 48.47/6.70 ![X0]: (r1(sK16_skl(X0)))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f78])).
% 48.47/6.70 fof(f91,plain,(
% 48.47/6.70 (![Y1,Y3,Y2,Y4]: ((![Y5]: (~id(Y4,Y5)|~r4(Y2,Y2,Y5)))|(![Y6]: (~r4(Y3,Y3,Y6)|(![Y7]: (~r4(Y1,Y1,Y7)|~r3(Y7,Y6,Y4)))))))),
% 48.47/6.70 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 48.47/6.70 fof(f92,plain,(
% 48.47/6.70 ![Y4]: ((![Y5]: (~id(Y4,Y5)|(![Y2]: ~r4(Y2,Y2,Y5))))|(![Y6]: ((![Y3]: ~r4(Y3,Y3,Y6))|(![Y7]: ((![Y1]: ~r4(Y1,Y1,Y7))|~r3(Y7,Y6,Y4))))))),
% 48.47/6.70 inference(miniscoping,[status(thm)],[f91])).
% 48.47/6.70 fof(f93,plain,(
% 48.47/6.70 ![X0,X1,X2,X3,X4,X5,X6]: (~id(X0,X1)|~r4(X2,X2,X1)|~r4(X3,X3,X4)|~r4(X5,X5,X6)|~r3(X6,X4,X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f92])).
% 48.47/6.70 fof(f94,plain,(
% 48.47/6.70 ![Y24,X19]: ((~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19)))&(sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 48.47/6.70 inference(NNF_transformation,[status(thm)],[f21])).
% 48.47/6.70 fof(f95,plain,(
% 48.47/6.70 (![Y24,X19]: (~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19))))&(![Y24,X19]: (sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 48.47/6.70 inference(miniscoping,[status(thm)],[f94])).
% 48.47/6.70 fof(f96,plain,(
% 48.47/6.70 ![X0,X1]: (~sP0_prd(X0,X1)|id(X0,X1))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f95])).
% 48.47/6.70 fof(f104,plain,(
% 48.47/6.70 ![X13,X14,Y22,X15]: ((~sP2_prd(X15,Y22,X14,X13)|(id(X15,Y22)&r3(X13,X14,X15)))&(sP2_prd(X15,Y22,X14,X13)|(~id(X15,Y22)|~r3(X13,X14,X15))))),
% 48.47/6.70 inference(NNF_transformation,[status(thm)],[f31])).
% 48.47/6.70 fof(f105,plain,(
% 48.47/6.70 (![X13,X14,Y22,X15]: (~sP2_prd(X15,Y22,X14,X13)|(id(X15,Y22)&r3(X13,X14,X15))))&(![X13,X14,Y22,X15]: (sP2_prd(X15,Y22,X14,X13)|(~id(X15,Y22)|~r3(X13,X14,X15))))),
% 48.47/6.70 inference(miniscoping,[status(thm)],[f104])).
% 48.47/6.70 fof(f106,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (~sP2_prd(X0,X1,X2,X3)|id(X0,X1))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f105])).
% 48.47/6.70 fof(f107,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (~sP2_prd(X0,X1,X2,X3)|r3(X3,X2,X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f105])).
% 48.47/6.70 fof(f109,plain,(
% 48.47/6.70 ![X16,X17,Y23,X18]: ((~sP3_prd(X18,Y23,X17,X16)|(id(X18,Y23)&r4(X16,X17,X18)))&(sP3_prd(X18,Y23,X17,X16)|(~id(X18,Y23)|~r4(X16,X17,X18))))),
% 48.47/6.70 inference(NNF_transformation,[status(thm)],[f36])).
% 48.47/6.70 fof(f110,plain,(
% 48.47/6.70 (![X16,X17,Y23,X18]: (~sP3_prd(X18,Y23,X17,X16)|(id(X18,Y23)&r4(X16,X17,X18))))&(![X16,X17,Y23,X18]: (sP3_prd(X18,Y23,X17,X16)|(~id(X18,Y23)|~r4(X16,X17,X18))))),
% 48.47/6.70 inference(miniscoping,[status(thm)],[f109])).
% 48.47/6.70 fof(f111,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (~sP3_prd(X0,X1,X2,X3)|id(X0,X1))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f110])).
% 48.47/6.70 fof(f112,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (~sP3_prd(X0,X1,X2,X3)|r4(X3,X2,X0))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f110])).
% 48.47/6.70 fof(f114,plain,(
% 48.47/6.70 ![X26,X27]: ((~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27)))&(sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 48.47/6.70 inference(NNF_transformation,[status(thm)],[f45])).
% 48.47/6.70 fof(f115,plain,(
% 48.47/6.70 (![X26,X27]: (~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27))))&(![X26,X27]: (sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 48.47/6.70 inference(miniscoping,[status(thm)],[f114])).
% 48.47/6.70 fof(f116,plain,(
% 48.47/6.70 ![X0,X1]: (~sP4_prd(X0,X1)|~r1(X1))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f115])).
% 48.47/6.70 fof(f129,plain,(
% 48.47/6.70 ![X38,X39,X40,X41,X42,X43]: ((~sP7_prd(X43,X42,X41,X40,X39,X38)|(~r4(X38,X39,X40)&~r4(X41,X42,X43)))&(sP7_prd(X43,X42,X41,X40,X39,X38)|(r4(X38,X39,X40)|r4(X41,X42,X43))))),
% 48.47/6.70 inference(NNF_transformation,[status(thm)],[f57])).
% 48.47/6.70 fof(f130,plain,(
% 48.47/6.70 (![X38,X39,X40,X41,X42,X43]: (~sP7_prd(X43,X42,X41,X40,X39,X38)|(~r4(X38,X39,X40)&~r4(X41,X42,X43))))&(![X38,X39,X40,X41,X42,X43]: (sP7_prd(X43,X42,X41,X40,X39,X38)|(r4(X38,X39,X40)|r4(X41,X42,X43))))),
% 48.47/6.70 inference(miniscoping,[status(thm)],[f129])).
% 48.47/6.70 fof(f131,plain,(
% 48.47/6.70 ![X0,X1,X2,X3,X4,X5]: (~sP7_prd(X0,X1,X2,X3,X4,X5)|~r4(X5,X4,X3))),
% 48.47/6.70 inference(cnf_transformation,[status(thm)],[f130])).
% 48.47/6.70 fof(f142,plain,(
% 48.47/6.70 ![X0,X1]: (sP0_prd(X0,sK0_skl)|~id(X0,X1)|~id(X1,sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f25,f44])).
% 48.47/6.70 fof(f146,plain,(
% 48.47/6.70 ![X0,X1,X2,X3,X4,X5]: (~r4(X0,X0,X1)|~r4(X2,X2,X3)|~r4(X4,X4,X5)|~r3(X5,X3,sK12_skl(X1)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f75,f93])).
% 48.47/6.70 fof(f148,plain,(
% 48.47/6.70 ![X0]: (sP0_prd(X0,sK0_skl)|~id(X0,sK12_skl(sK0_skl)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f142,f75])).
% 48.47/6.70 fof(f163,plain,(
% 48.47/6.70 ![X0]: (sP0_prd(X0,sK0_skl)|~id(sK12_skl(sK0_skl),X0))),
% 48.47/6.70 inference(resolution,[status(thm)],[f148,f42])).
% 48.47/6.70 fof(f176,plain,(
% 48.47/6.70 ![X0]: (sP2_prd(sK12_skl(X0),sK2_skl(sK13_skl(X0),X0),sK13_skl(X0),X0))),
% 48.47/6.70 inference(resolution,[status(thm)],[f77,f34])).
% 48.47/6.70 fof(f184,plain,(
% 48.47/6.70 ![X0,X1]: (sP4_prd(X0,X1)|r1(X0)|~id(X0,X1))),
% 48.47/6.70 inference(resolution,[status(thm)],[f48,f42])).
% 48.47/6.70 fof(f250,plain,(
% 48.47/6.70 ![X0]: (sP0_prd(sK13_skl(X0),sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f76,f24])).
% 48.47/6.70 fof(f251,plain,(
% 48.47/6.70 ![X0]: (sP0_prd(sK15_skl(X0),sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f79,f24])).
% 48.47/6.70 fof(f270,plain,(
% 48.47/6.70 ![X0]: (sP4_prd(sK14_skl(X0),sK16_skl(X0))|r1(sK14_skl(X0)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f81,f184])).
% 48.47/6.70 fof(f365,plain,(
% 48.47/6.70 ![X0,X1,X2]: (r3(X0,X1,X2)|~id(X2,sK2_skl(X1,X0)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f107,f35])).
% 48.47/6.70 fof(f384,plain,(
% 48.47/6.70 ![X0,X1,X2]: (r4(X0,X1,X2)|~id(X2,sK3_skl(X1,X0)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f112,f40])).
% 48.47/6.70 fof(f388,plain,(
% 48.47/6.70 ![X0,X1]: (~sP4_prd(X0,sK16_skl(X1)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f116,f82])).
% 48.47/6.70 fof(f562,plain,(
% 48.47/6.70 ![X0,X1,X2,X3,X4,X5]: (~r4(X0,X1,X2)|~id(X0,X3)|~id(X1,X4)|~id(X2,X5)|r4(X3,X4,X5))),
% 48.47/6.70 inference(resolution,[status(thm)],[f131,f60])).
% 48.47/6.70 fof(f641,plain,(
% 48.47/6.70 ![X0,X1,X2]: (r3(X0,X1,X2)|~id(sK2_skl(X1,X0),X2))),
% 48.47/6.70 inference(resolution,[status(thm)],[f365,f42])).
% 48.47/6.70 fof(f644,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (r4(X0,X1,X2)|~id(X2,X3)|~id(X3,sK3_skl(X1,X0)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f384,f44])).
% 48.47/6.70 fof(f723,plain,(
% 48.47/6.70 ![X0,X1,X2]: (~r4(X0,X1,X2)|id(X2,sK3_skl(X1,X0)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f39,f111])).
% 48.47/6.70 fof(f727,plain,(
% 48.47/6.70 ![X0]: (id(sK12_skl(X0),sK2_skl(sK13_skl(X0),X0)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f176,f106])).
% 48.47/6.70 fof(f731,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (r3(X0,X1,X2)|~id(sK2_skl(X1,X0),X3)|~id(X3,X2))),
% 48.47/6.70 inference(resolution,[status(thm)],[f641,f44])).
% 48.47/6.70 fof(f871,plain,(
% 48.47/6.70 ![X0]: (id(sK13_skl(X0),sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f250,f96])).
% 48.47/6.70 fof(f873,plain,(
% 48.47/6.70 ![X0]: (id(sK15_skl(X0),sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f251,f96])).
% 48.47/6.70 fof(f1032,plain,(
% 48.47/6.70 ![X0]: (r1(sK14_skl(X0)))),
% 48.47/6.70 inference(backward_subsumption_resolution,[status(thm)],[f270,f388])).
% 48.47/6.70 fof(f1337,plain,(
% 48.47/6.70 ![X0]: (~r1(X0)|id(X0,sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f24,f96])).
% 48.47/6.70 fof(f1461,plain,(
% 48.47/6.70 ![X0]: (id(sK14_skl(X0),sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f1032,f1337])).
% 48.47/6.70 fof(f1580,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (~id(X0,X1)|~id(sK15_skl(X0),X2)|~id(sK14_skl(X0),X3)|r4(X1,X2,X3))),
% 48.47/6.70 inference(resolution,[status(thm)],[f562,f80])).
% 48.47/6.70 fof(f2851,plain,(
% 48.47/6.70 sP0_prd(sK2_skl(sK13_skl(sK0_skl),sK0_skl),sK0_skl)),
% 48.47/6.70 inference(resolution,[status(thm)],[f163,f727])).
% 48.47/6.70 fof(f2869,plain,(
% 48.47/6.70 id(sK2_skl(sK13_skl(sK0_skl),sK0_skl),sK0_skl)),
% 48.47/6.70 inference(resolution,[status(thm)],[f2851,f96])).
% 48.47/6.70 fof(f3129,plain,(
% 48.47/6.70 ![X0,X1,X2]: (~id(X0,X1)|~id(sK14_skl(X0),X2)|r4(X1,sK0_skl,X2))),
% 48.47/6.70 inference(resolution,[status(thm)],[f1580,f873])).
% 48.47/6.70 fof(f3564,plain,(
% 48.47/6.70 ![X0]: (r3(sK0_skl,sK13_skl(sK0_skl),X0)|~id(sK0_skl,X0))),
% 48.47/6.70 inference(resolution,[status(thm)],[f731,f2869])).
% 48.47/6.70 fof(f4404,plain,(
% 48.47/6.70 ![X0,X1,X2,X3]: (~id(sK0_skl,sK12_skl(X0))|~r4(X1,X1,X0)|~r4(X2,X2,sK13_skl(sK0_skl))|~r4(X3,X3,sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f3564,f146])).
% 48.47/6.70 fof(f4408,definition,(
% 48.47/6.70 ![X0,X1]: (sQ105_spl <=> (~id(sK0_skl,sK12_skl(X0))|~r4(X1,X1,X0)))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 48.47/6.70 fof(f4409,plain,(
% 48.47/6.70 ![X0,X1]: (~id(sK0_skl,sK12_skl(X0))|~r4(X1,X1,X0)|~sQ105_spl)),
% 48.47/6.70 inference(component_clause,[status(thm)],[f4408])).
% 48.47/6.70 fof(f4411,definition,(
% 48.47/6.70 ![X2]: (sQ106_spl <=> (~r4(X2,X2,sK13_skl(sK0_skl))))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 48.47/6.70 fof(f4412,plain,(
% 48.47/6.70 ![X0]: (~r4(X0,X0,sK13_skl(sK0_skl))|~sQ106_spl)),
% 48.47/6.70 inference(component_clause,[status(thm)],[f4411])).
% 48.47/6.70 fof(f4414,definition,(
% 48.47/6.70 ![X3]: (sQ107_spl <=> (~r4(X3,X3,sK0_skl)))),
% 48.47/6.70 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 48.47/6.70 fof(f4415,plain,(
% 48.47/6.70 ![X0]: (~r4(X0,X0,sK0_skl)|~sQ107_spl)),
% 48.47/6.70 inference(component_clause,[status(thm)],[f4414])).
% 48.47/6.70 fof(f4417,plain,(
% 48.47/6.70 sQ105_spl|sQ106_spl|sQ107_spl),
% 48.47/6.70 inference(split_clause,[status(thm)],[f4404,f4408,f4411,f4414])).
% 48.47/6.70 fof(f7730,plain,(
% 48.47/6.70 ![X0,X1]: (~id(X0,X1)|r4(X1,sK0_skl,sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f3129,f1461])).
% 48.47/6.70 fof(f7770,plain,(
% 48.47/6.70 r4(sK0_skl,sK0_skl,sK0_skl)),
% 48.47/6.70 inference(resolution,[status(thm)],[f7730,f2869])).
% 48.47/6.70 fof(f7798,plain,(
% 48.47/6.70 ![X0]: (r4(X0,sK0_skl,sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f7730,f75])).
% 48.47/6.70 fof(f7807,plain,(
% 48.47/6.70 $false|~sQ107_spl),
% 48.47/6.70 inference(forward_subsumption_resolution,[status(thm)],[f7770,f4415])).
% 48.47/6.70 fof(f7808,plain,(
% 48.47/6.70 ~sQ107_spl),
% 48.47/6.70 inference(contradiction_clause,[status(thm)],[f7807])).
% 48.47/6.70 fof(f7890,plain,(
% 48.47/6.70 ![X0]: (id(sK0_skl,sK3_skl(sK0_skl,X0)))),
% 48.47/6.70 inference(resolution,[status(thm)],[f7798,f723])).
% 48.47/6.70 fof(f8155,plain,(
% 48.47/6.70 ![X0,X1]: (~r4(X0,X0,X1)|~id(sK12_skl(X1),sK0_skl)|~sQ105_spl)),
% 48.47/6.70 inference(resolution,[status(thm)],[f4409,f42])).
% 48.47/6.70 fof(f8211,plain,(
% 48.47/6.70 ![X0,X1]: (r4(X0,sK0_skl,X1)|~id(X1,sK0_skl))),
% 48.47/6.70 inference(resolution,[status(thm)],[f7890,f644])).
% 48.47/6.70 fof(f8576,plain,(
% 48.47/6.70 ![X0,X1]: (r4(X0,sK0_skl,sK13_skl(X1)))),
% 48.47/6.73 inference(resolution,[status(thm)],[f8211,f871])).
% 48.47/6.73 fof(f8697,plain,(
% 48.47/6.73 ~id(sK12_skl(sK0_skl),sK0_skl)|~sQ105_spl),
% 48.47/6.73 inference(resolution,[status(thm)],[f8155,f7798])).
% 48.47/6.73 fof(f8701,plain,(
% 48.47/6.73 $false|~sQ105_spl),
% 48.47/6.73 inference(forward_subsumption_resolution,[status(thm)],[f8697,f75])).
% 48.47/6.73 fof(f8702,plain,(
% 48.47/6.73 ~sQ105_spl),
% 48.47/6.73 inference(contradiction_clause,[status(thm)],[f8701])).
% 48.47/6.73 fof(f9106,plain,(
% 48.47/6.73 $false|~sQ106_spl),
% 48.47/6.73 inference(resolution,[status(thm)],[f4412,f8576])).
% 48.47/6.73 fof(f9107,plain,(
% 48.47/6.73 ~sQ106_spl),
% 48.47/6.73 inference(contradiction_clause,[status(thm)],[f9106])).
% 48.47/6.73 fof(f9108,plain,(
% 48.47/6.73 $false),
% 48.47/6.73 inference(sat_refutation,[status(thm)],[f4417,f7808,f8702,f9107])).
% 48.47/6.73 % SZS output end CNFRefutation for theBenchmark.p
% 12.76/6.76 % Elapsed time: 6.375245 seconds
% 12.76/6.76 % CPU time: 50.289819 seconds
% 12.76/6.76 % Total memory used: 294.044 MB
% 12.76/6.76 % Net memory used: 230.832 MB
%------------------------------------------------------------------------------