%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUN065+1 : 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 : n005.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 208.68s 41.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN065+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/15.40 % Computer : n005.cluster.edu
% 0.13/15.40 % Model : x86_64 x86_64
% 0.13/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/15.40 % Memory : 8046.5625MB
% 0.13/15.40 % OS : Linux 6.8.0-71-generic
% 0.13/15.40 % CPULimit : 300
% 0.13/15.40 % WCLimit : 300
% 0.13/15.41 % DateTime : Mon Sep 21 03:23:19 UTC 2026
% 0.13/15.41 % CPUTime :
% 0.13/15.42 % Drodi V4.1.1
% 208.68/41.84 % Refutation found
% 208.68/41.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 208.68/41.84 % SZS output start CNFRefutation for theBenchmark
% 208.68/41.84 fof(f1,axiom,(
% 208.68/41.84 (? [Y24] :(! [X19] :( ( id(X19,Y24)& r1(X19) )| ( ~ r1(X19)& ~ id(X19,Y24) ) ) ))),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f2,axiom,(
% 208.68/41.84 (! [X11] :(? [Y21] :(! [X12] :( ( id(X12,Y21)& r2(X11,X12) )| ( ~ r2(X11,X12)& ~ id(X12,Y21) ) ) )))),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f3,axiom,(
% 208.68/41.84 (! [X13,X14] :(? [Y22] :(! [X15] :( ( id(X15,Y22)& r3(X13,X14,X15) )| ( ~ r3(X13,X14,X15)& ~ id(X15,Y22) ) ) )))),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f5,axiom,(
% 208.68/41.84 (! [X20] : id(X20,X20) )),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f6,axiom,(
% 208.68/41.84 (! [X21,X22] :( ~ id(X21,X22)| id(X22,X21) ) )),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f7,axiom,(
% 208.68/41.84 (! [X23,X24,X25] :( ~ id(X23,X24)| id(X23,X25)| ~ id(X24,X25) ) )),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f8,axiom,(
% 208.68/41.84 (! [X26,X27] :( ~ id(X26,X27)| ( ~ r1(X26)& ~ r1(X27) )| ( r1(X26)& r1(X27) ) ) )),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f14,axiom,(
% 208.68/41.84 (! [X3,X10] :( (! [Y12] :( (! [Y13] :( ~ id(Y13,Y12)| ~ r2(X3,Y13) ))| ~ r2(X10,Y12) ))| id(X3,X10) ) )),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f15,axiom,(
% 208.68/41.84 (! [X4] :(? [Y9] :( id(Y9,X4)& (? [Y16] :( r1(Y16)& r3(X4,Y16,Y9) ) )) ))),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f18,axiom,(
% 208.68/41.84 (! [X7,Y10] :( (! [Y20] :( ~ id(Y20,Y10)| ~ r1(Y20) ))| ~ r2(X7,Y10) ) )),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f19,conjecture,(
% 208.68/41.84 (? [Y1] :( (! [Y2] :( (! [Y3] :( ~ r1(Y3)| ~ r2(Y3,Y2) ))| ~ id(Y1,Y2) ))& (! [Y4] :( ~ id(Y1,Y4)| ~ r1(Y4) ) )) )),
% 208.68/41.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 208.68/41.84 fof(f20,negated_conjecture,(
% 208.68/41.84 ~((? [Y1] :( (! [Y2] :( (! [Y3] :( ~ r1(Y3)| ~ r2(Y3,Y2) ))| ~ id(Y1,Y2) ))& (! [Y4] :( ~ id(Y1,Y4)| ~ r1(Y4) ) )) ))),
% 208.68/41.84 inference(negated_conjecture,[status(cth)],[f19])).
% 208.68/41.84 fof(f21,definition,(
% 208.68/41.84 ![Y24,X19]: (sP0_prd(X19,Y24)<=>(id(X19,Y24)&r1(X19)))),
% 208.68/41.84 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 208.68/41.84 fof(f22,plain,(
% 208.68/41.84 ?[Y24]: ![X19]: (sP0_prd(X19,Y24)|(~r1(X19)&~id(X19,Y24)))),
% 208.68/41.84 inference(formula_renaming,[status(thm)],[f1,f21])).
% 208.68/41.84 fof(f23,plain,(
% 208.68/41.84 ![X19]: (sP0_prd(X19,sK0_skl)|(~r1(X19)&~id(X19,sK0_skl)))),
% 208.68/41.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y24,sK0_skl)],[f22])).
% 208.68/41.84 fof(f24,plain,(
% 208.68/41.84 ![X0]: (sP0_prd(X0,sK0_skl)|~r1(X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f23])).
% 208.68/41.84 fof(f25,plain,(
% 208.68/41.84 ![X0]: (sP0_prd(X0,sK0_skl)|~id(X0,sK0_skl))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f23])).
% 208.68/41.84 fof(f26,definition,(
% 208.68/41.84 ![X11,Y21,X12]: (sP1_prd(X12,Y21,X11)<=>(id(X12,Y21)&r2(X11,X12)))),
% 208.68/41.84 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 208.68/41.84 fof(f27,plain,(
% 208.68/41.84 ![X11]: ?[Y21]: ![X12]: (sP1_prd(X12,Y21,X11)|(~r2(X11,X12)&~id(X12,Y21)))),
% 208.68/41.84 inference(formula_renaming,[status(thm)],[f2,f26])).
% 208.68/41.84 fof(f28,plain,(
% 208.68/41.84 ![X11]: ![X12]: (sP1_prd(X12,sK1_skl(X11),X11)|(~r2(X11,X12)&~id(X12,sK1_skl(X11))))),
% 208.68/41.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y21,sK1_skl(X11))],[f27])).
% 208.68/41.84 fof(f29,plain,(
% 208.68/41.84 ![X0,X1]: (sP1_prd(X0,sK1_skl(X1),X1)|~r2(X1,X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f28])).
% 208.68/41.84 fof(f30,plain,(
% 208.68/41.84 ![X0,X1]: (sP1_prd(X0,sK1_skl(X1),X1)|~id(X0,sK1_skl(X1)))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f28])).
% 208.68/41.84 fof(f31,definition,(
% 208.68/41.84 ![X13,X14,Y22,X15]: (sP2_prd(X15,Y22,X14,X13)<=>(id(X15,Y22)&r3(X13,X14,X15)))),
% 208.68/41.84 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 208.68/41.84 fof(f32,plain,(
% 208.68/41.84 ![X13,X14]: ?[Y22]: ![X15]: (sP2_prd(X15,Y22,X14,X13)|(~r3(X13,X14,X15)&~id(X15,Y22)))),
% 208.68/41.84 inference(formula_renaming,[status(thm)],[f3,f31])).
% 208.68/41.84 fof(f33,plain,(
% 208.68/41.84 ![X13,X14]: ![X15]: (sP2_prd(X15,sK2_skl(X14,X13),X14,X13)|(~r3(X13,X14,X15)&~id(X15,sK2_skl(X14,X13))))),
% 208.68/41.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y22,sK2_skl(X14,X13))],[f32])).
% 208.68/41.84 fof(f34,plain,(
% 208.68/41.84 ![X0,X1,X2]: (sP2_prd(X0,sK2_skl(X1,X2),X1,X2)|~r3(X2,X1,X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f33])).
% 208.68/41.84 fof(f41,plain,(
% 208.68/41.84 ![X0]: (id(X0,X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f5])).
% 208.68/41.84 fof(f42,plain,(
% 208.68/41.84 ![X0,X1]: (~id(X0,X1)|id(X1,X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f6])).
% 208.68/41.84 fof(f43,plain,(
% 208.68/41.84 ![X24,X25]: ((![X23]: (~id(X23,X24)|id(X23,X25)))|~id(X24,X25))),
% 208.68/41.84 inference(miniscoping,[status(thm)],[f7])).
% 208.68/41.84 fof(f44,plain,(
% 208.68/41.84 ![X0,X1,X2]: (~id(X0,X1)|id(X0,X2)|~id(X1,X2))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f43])).
% 208.68/41.84 fof(f45,definition,(
% 208.68/41.84 ![X26,X27]: (sP4_prd(X27,X26)<=>(~r1(X26)&~r1(X27)))),
% 208.68/41.84 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 208.68/41.84 fof(f46,plain,(
% 208.68/41.84 ![X26,X27]: ((~id(X26,X27)|sP4_prd(X27,X26))|(r1(X26)&r1(X27)))),
% 208.68/41.84 inference(formula_renaming,[status(thm)],[f8,f45])).
% 208.68/41.84 fof(f47,plain,(
% 208.68/41.84 ![X0,X1]: (~id(X0,X1)|sP4_prd(X1,X0)|r1(X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f46])).
% 208.68/41.84 fof(f48,plain,(
% 208.68/41.84 ![X0,X1]: (~id(X0,X1)|sP4_prd(X1,X0)|r1(X1))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f46])).
% 208.68/41.84 fof(f73,plain,(
% 208.68/41.84 ![X0,X1,X2,X3]: (~id(X0,X1)|~r2(X2,X0)|~r2(X3,X1)|id(X2,X3))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f14])).
% 208.68/41.84 fof(f74,plain,(
% 208.68/41.84 ![X4]: (id(sK12_skl(X4),X4)&(r1(sK13_skl(X4))&r3(X4,sK13_skl(X4),sK12_skl(X4))))),
% 208.68/41.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(Y9,sK12_skl(X4)),skolemize(Y16,sK13_skl(X4))],[f15])).
% 208.68/41.84 fof(f75,plain,(
% 208.68/41.84 ![X0]: (id(sK12_skl(X0),X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f74])).
% 208.68/41.84 fof(f77,plain,(
% 208.68/41.84 ![X0]: (r3(X0,sK13_skl(X0),sK12_skl(X0)))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f74])).
% 208.68/41.84 fof(f89,plain,(
% 208.68/41.84 ![Y10]: ((![Y20]: (~id(Y20,Y10)|~r1(Y20)))|(![X7]: ~r2(X7,Y10)))),
% 208.68/41.84 inference(miniscoping,[status(thm)],[f18])).
% 208.68/41.84 fof(f90,plain,(
% 208.68/41.84 ![X0,X1,X2]: (~id(X0,X1)|~r1(X0)|~r2(X2,X1))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f89])).
% 208.68/41.84 fof(f91,plain,(
% 208.68/41.84 (![Y1]: ((?[Y2]: ((?[Y3]: (r1(Y3)&r2(Y3,Y2)))&id(Y1,Y2)))|(?[Y4]: (id(Y1,Y4)&r1(Y4)))))),
% 208.68/41.84 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 208.68/41.84 fof(f92,definition,(
% 208.68/41.84 ![Y1,Y2]: (sP9_prd(Y2,Y1)<=>((?[Y3]: (r1(Y3)&r2(Y3,Y2)))&id(Y1,Y2)))),
% 208.68/41.84 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 208.68/41.84 fof(f93,plain,(
% 208.68/41.84 ![Y1]: ((?[Y2]: sP9_prd(Y2,Y1))|(?[Y4]: (id(Y1,Y4)&r1(Y4))))),
% 208.68/41.84 inference(formula_renaming,[status(thm)],[f91,f92])).
% 208.68/41.84 fof(f94,plain,(
% 208.68/41.84 ![Y1]: (sP9_prd(sK20_skl(Y1),Y1)|(id(Y1,sK21_skl(Y1))&r1(sK21_skl(Y1))))),
% 208.68/41.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl]),skolemize(Y2,sK20_skl(Y1)),skolemize(Y4,sK21_skl(Y1))],[f93])).
% 208.68/41.84 fof(f95,plain,(
% 208.68/41.84 ![X0]: (sP9_prd(sK20_skl(X0),X0)|id(X0,sK21_skl(X0)))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f94])).
% 208.68/41.84 fof(f96,plain,(
% 208.68/41.84 ![X0]: (sP9_prd(sK20_skl(X0),X0)|r1(sK21_skl(X0)))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f94])).
% 208.68/41.84 fof(f97,plain,(
% 208.68/41.84 ![Y24,X19]: ((~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19)))&(sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 208.68/41.84 inference(NNF_transformation,[status(thm)],[f21])).
% 208.68/41.84 fof(f98,plain,(
% 208.68/41.84 (![Y24,X19]: (~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19))))&(![Y24,X19]: (sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 208.68/41.84 inference(miniscoping,[status(thm)],[f97])).
% 208.68/41.84 fof(f99,plain,(
% 208.68/41.84 ![X0,X1]: (~sP0_prd(X0,X1)|id(X0,X1))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f98])).
% 208.68/41.84 fof(f100,plain,(
% 208.68/41.84 ![X0,X1]: (~sP0_prd(X0,X1)|r1(X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f98])).
% 208.68/41.84 fof(f102,plain,(
% 208.68/41.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))))),
% 208.68/41.84 inference(NNF_transformation,[status(thm)],[f26])).
% 208.68/41.84 fof(f103,plain,(
% 208.68/41.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))))),
% 208.68/41.84 inference(miniscoping,[status(thm)],[f102])).
% 208.68/41.84 fof(f104,plain,(
% 208.68/41.84 ![X0,X1,X2]: (~sP1_prd(X0,X1,X2)|id(X0,X1))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f103])).
% 208.68/41.84 fof(f105,plain,(
% 208.68/41.84 ![X0,X1,X2]: (~sP1_prd(X0,X1,X2)|r2(X2,X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f103])).
% 208.68/41.84 fof(f107,plain,(
% 208.68/41.84 ![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))))),
% 208.68/41.84 inference(NNF_transformation,[status(thm)],[f31])).
% 208.68/41.84 fof(f108,plain,(
% 208.68/41.84 (![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))))),
% 208.68/41.84 inference(miniscoping,[status(thm)],[f107])).
% 208.68/41.84 fof(f109,plain,(
% 208.68/41.84 ![X0,X1,X2,X3]: (~sP2_prd(X0,X1,X2,X3)|id(X0,X1))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f108])).
% 208.68/41.84 fof(f117,plain,(
% 208.68/41.84 ![X26,X27]: ((~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27)))&(sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 208.68/41.84 inference(NNF_transformation,[status(thm)],[f45])).
% 208.68/41.84 fof(f118,plain,(
% 208.68/41.84 (![X26,X27]: (~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27))))&(![X26,X27]: (sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 208.68/41.84 inference(miniscoping,[status(thm)],[f117])).
% 208.68/41.84 fof(f119,plain,(
% 208.68/41.84 ![X0,X1]: (~sP4_prd(X0,X1)|~r1(X1))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f118])).
% 208.68/41.84 fof(f120,plain,(
% 208.68/41.84 ![X0,X1]: (~sP4_prd(X0,X1)|~r1(X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f118])).
% 208.68/41.84 fof(f142,plain,(
% 208.68/41.84 ![Y1,Y2]: ((~sP9_prd(Y2,Y1)|((?[Y3]: (r1(Y3)&r2(Y3,Y2)))&id(Y1,Y2)))&(sP9_prd(Y2,Y1)|((![Y3]: (~r1(Y3)|~r2(Y3,Y2)))|~id(Y1,Y2))))),
% 208.68/41.84 inference(NNF_transformation,[status(thm)],[f92])).
% 208.68/41.84 fof(f143,plain,(
% 208.68/41.84 (![Y1,Y2]: (~sP9_prd(Y2,Y1)|((?[Y3]: (r1(Y3)&r2(Y3,Y2)))&id(Y1,Y2))))&(![Y1,Y2]: (sP9_prd(Y2,Y1)|((![Y3]: (~r1(Y3)|~r2(Y3,Y2)))|~id(Y1,Y2))))),
% 208.68/41.84 inference(miniscoping,[status(thm)],[f142])).
% 208.68/41.84 fof(f144,plain,(
% 208.68/41.84 (![Y1,Y2]: (~sP9_prd(Y2,Y1)|((r1(sK22_skl(Y2,Y1))&r2(sK22_skl(Y2,Y1),Y2))&id(Y1,Y2))))&(![Y1,Y2]: (sP9_prd(Y2,Y1)|((![Y3]: (~r1(Y3)|~r2(Y3,Y2)))|~id(Y1,Y2))))),
% 208.68/41.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(Y3,sK22_skl(Y2,Y1))],[f143])).
% 208.68/41.84 fof(f145,plain,(
% 208.68/41.84 ![X0,X1]: (~sP9_prd(X0,X1)|r1(sK22_skl(X0,X1)))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f144])).
% 208.68/41.84 fof(f146,plain,(
% 208.68/41.84 ![X0,X1]: (~sP9_prd(X0,X1)|r2(sK22_skl(X0,X1),X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f144])).
% 208.68/41.84 fof(f147,plain,(
% 208.68/41.84 ![X0,X1]: (~sP9_prd(X0,X1)|id(X1,X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f144])).
% 208.68/41.84 fof(f148,plain,(
% 208.68/41.84 ![X0,X1,X2]: (sP9_prd(X0,X1)|~r1(X2)|~r2(X2,X0)|~id(X1,X0))),
% 208.68/41.84 inference(cnf_transformation,[status(thm)],[f144])).
% 208.68/41.84 fof(f150,plain,(
% 208.68/41.84 ![X0,X1,X2,X3]: (sP9_prd(X0,X1)|~r2(sK22_skl(X2,X3),X0)|~id(X1,X0)|~sP9_prd(X2,X3))),
% 208.68/41.84 inference(resolution,[status(thm)],[f148,f145])).
% 208.68/41.84 fof(f153,plain,(
% 208.68/41.84 ![X0,X1,X2]: (sP9_prd(X0,X1)|~id(X1,X0)|~sP9_prd(X0,X2)|~sP9_prd(X0,X2))),
% 208.68/41.84 inference(resolution,[status(thm)],[f150,f146])).
% 208.68/41.84 fof(f154,plain,(
% 208.68/41.84 ![X0,X1,X2]: (sP9_prd(X0,X1)|~id(X1,X0)|~sP9_prd(X0,X2))),
% 208.68/41.84 inference(duplicate_literals_removal,[status(thm)],[f153])).
% 208.68/41.84 fof(f155,plain,(
% 208.68/41.84 ![X0,X1]: (sP9_prd(sK20_skl(X0),X1)|~id(X1,sK20_skl(X0))|r1(sK21_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f154,f96])).
% 208.68/41.84 fof(f171,plain,(
% 208.68/41.84 sP0_prd(sK0_skl,sK0_skl)),
% 208.68/41.84 inference(resolution,[status(thm)],[f25,f41])).
% 208.68/41.84 fof(f180,plain,(
% 208.68/41.84 r1(sK0_skl)),
% 208.68/41.84 inference(resolution,[status(thm)],[f171,f100])).
% 208.68/41.84 fof(f182,plain,(
% 208.68/41.84 ![X0,X1]: (~id(sK0_skl,X0)|~r2(X1,X0))),
% 208.68/41.84 inference(resolution,[status(thm)],[f180,f90])).
% 208.68/41.84 fof(f209,plain,(
% 208.68/41.84 ![X0]: (id(X0,sK0_skl)|~r1(X0))),
% 208.68/41.84 inference(resolution,[status(thm)],[f99,f24])).
% 208.68/41.84 fof(f255,plain,(
% 208.68/41.84 ![X0,X1]: (id(X0,sK1_skl(X1))|~r2(X1,X0))),
% 208.68/41.84 inference(resolution,[status(thm)],[f104,f29])).
% 208.68/41.84 fof(f256,plain,(
% 208.68/41.84 ![X0,X1]: (r2(X0,X1)|~id(X1,sK1_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f105,f30])).
% 208.68/41.84 fof(f277,plain,(
% 208.68/41.84 ![X0]: (sP4_prd(sK21_skl(X0),X0)|r1(X0)|sP9_prd(sK20_skl(X0),X0))),
% 208.68/41.84 inference(resolution,[status(thm)],[f47,f95])).
% 208.68/41.84 fof(f280,plain,(
% 208.68/41.84 ![X0,X1]: (sP4_prd(X0,X1)|r1(X1)|~id(X0,X1))),
% 208.68/41.84 inference(resolution,[status(thm)],[f47,f42])).
% 208.68/41.84 fof(f287,plain,(
% 208.68/41.84 ![X0,X1,X2,X3]: (sP4_prd(X0,X1)|r1(X0)|~id(X2,X3)|~r2(X1,X2)|~r2(X0,X3))),
% 208.68/41.84 inference(resolution,[status(thm)],[f48,f73])).
% 208.68/41.84 fof(f289,plain,(
% 208.68/41.84 ![X0,X1]: (sP4_prd(X0,X1)|r1(X0)|~id(X0,X1))),
% 208.68/41.84 inference(resolution,[status(thm)],[f48,f42])).
% 208.68/41.84 fof(f297,plain,(
% 208.68/41.84 ![X0,X1]: (sP4_prd(sK21_skl(X0),X0)|r1(X0)|sP9_prd(sK20_skl(X0),X1)|~id(X1,sK20_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f277,f154])).
% 208.68/41.84 fof(f402,plain,(
% 208.68/41.84 ![X0,X1,X2]: (id(X0,sK2_skl(X1,X2))|~r3(X2,X1,X0))),
% 208.68/41.84 inference(resolution,[status(thm)],[f109,f34])).
% 208.68/41.84 fof(f412,plain,(
% 208.68/41.84 ![X0,X1]: (~r2(X0,X1)|sP4_prd(X1,sK1_skl(X0))|r1(sK1_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f255,f280])).
% 208.68/41.84 fof(f418,plain,(
% 208.68/41.84 ![X0,X1,X2]: (r2(X0,X1)|~id(X1,X2)|~id(X2,sK1_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f256,f44])).
% 208.68/41.84 fof(f419,plain,(
% 208.68/41.84 ![X0,X1]: (r2(X0,X1)|~id(sK1_skl(X0),X1))),
% 208.68/41.84 inference(resolution,[status(thm)],[f256,f42])).
% 208.68/41.84 fof(f420,plain,(
% 208.68/41.84 ![X0]: (r2(X0,sK1_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f256,f41])).
% 208.68/41.84 fof(f431,plain,(
% 208.68/41.84 ![X0]: (~id(sK0_skl,sK1_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f420,f182])).
% 208.68/41.84 fof(f436,plain,(
% 208.68/41.84 ![X0]: (~id(sK1_skl(X0),sK0_skl))),
% 208.68/41.84 inference(resolution,[status(thm)],[f431,f42])).
% 208.68/41.84 fof(f441,plain,(
% 208.68/41.84 ![X0]: (~r1(sK1_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f436,f209])).
% 208.68/41.84 fof(f459,plain,(
% 208.68/41.84 ![X0,X1,X2,X3]: (r1(X0)|~id(X1,X2)|~r2(X3,X1)|~r2(X0,X2)|~r1(X3))),
% 208.68/41.84 inference(resolution,[status(thm)],[f287,f119])).
% 208.68/41.84 fof(f534,plain,(
% 208.68/41.84 ![X0]: (sP4_prd(X0,sK21_skl(X0))|r1(X0)|sP9_prd(sK20_skl(X0),X0))),
% 208.68/41.84 inference(resolution,[status(thm)],[f289,f95])).
% 208.68/41.84 fof(f551,plain,(
% 208.68/41.84 ![X0,X1]: (r2(X0,X1)|~sP9_prd(X1,sK1_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f419,f147])).
% 208.68/41.84 fof(f573,plain,(
% 208.68/41.84 ![X0]: (r2(X0,sK20_skl(sK1_skl(X0)))|r1(sK21_skl(sK1_skl(X0))))),
% 208.68/41.84 inference(resolution,[status(thm)],[f551,f96])).
% 208.68/41.84 fof(f1264,plain,(
% 208.68/41.84 ![X0]: (id(sK12_skl(X0),sK2_skl(sK13_skl(X0),X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f402,f77])).
% 208.68/41.84 fof(f1727,plain,(
% 208.68/41.84 ![X0]: (sP4_prd(sK1_skl(X0),sK21_skl(sK1_skl(X0)))|r1(sK1_skl(X0))|r2(X0,sK20_skl(sK1_skl(X0))))),
% 208.68/41.84 inference(resolution,[status(thm)],[f534,f551])).
% 208.68/41.84 fof(f1753,plain,(
% 208.68/41.84 ![X0]: (sP4_prd(sK1_skl(X0),sK21_skl(sK1_skl(X0)))|r2(X0,sK20_skl(sK1_skl(X0))))),
% 208.68/41.84 inference(forward_subsumption_resolution,[status(thm)],[f1727,f441])).
% 208.68/41.84 fof(f1882,plain,(
% 208.68/41.84 ![X0,X1]: (~r2(X0,X1)|sP4_prd(X1,sK1_skl(X0)))),
% 208.68/41.84 inference(forward_subsumption_resolution,[status(thm)],[f412,f441])).
% 208.68/41.84 fof(f1883,plain,(
% 208.68/41.84 ![X0,X1]: (~r2(X0,X1)|~r1(X1))),
% 208.68/41.84 inference(resolution,[status(thm)],[f1882,f120])).
% 208.68/41.84 fof(f1998,plain,(
% 208.68/41.84 ![X0,X1]: (r2(X0,X1)|~id(X1,sK12_skl(sK1_skl(X0))))),
% 208.68/41.84 inference(resolution,[status(thm)],[f418,f75])).
% 208.68/41.84 fof(f2121,plain,(
% 208.68/41.84 ![X0,X1,X2,X3]: (r1(X0)|~id(X1,X2)|~r2(X0,X2)|~r1(sK22_skl(X1,X3))|~sP9_prd(X1,X3))),
% 208.68/41.84 inference(resolution,[status(thm)],[f459,f146])).
% 208.68/41.84 fof(f2126,plain,(
% 208.68/41.84 ![X0,X1,X2,X3]: (r1(X0)|~id(X1,X2)|~r2(X0,X2)|~sP9_prd(X1,X3))),
% 208.68/41.84 inference(forward_subsumption_resolution,[status(thm)],[f2121,f145])).
% 208.68/41.84 fof(f4703,plain,(
% 208.68/41.84 ![X0,X1]: (r1(X0)|sP9_prd(sK20_skl(X0),X1)|~id(X1,sK20_skl(X0))|~r1(sK21_skl(X0)))),
% 208.68/41.84 inference(resolution,[status(thm)],[f297,f120])).
% 208.68/41.84 fof(f4705,plain,(
% 208.68/41.84 ![X0,X1]: (r1(X0)|sP9_prd(sK20_skl(X0),X1)|~id(X1,sK20_skl(X0)))),
% 208.68/41.84 inference(forward_subsumption_resolution,[status(thm)],[f4703,f155])).
% 208.68/41.84 fof(f6095,plain,(
% 208.68/41.84 ![X0,X1]: (r2(X0,X1)|~id(sK12_skl(sK1_skl(X0)),X1))),
% 208.68/41.84 inference(resolution,[status(thm)],[f1998,f42])).
% 208.68/41.84 fof(f8501,plain,(
% 208.68/41.84 ![X0]: (r2(X0,sK2_skl(sK13_skl(sK1_skl(X0)),sK1_skl(X0))))),
% 208.68/41.84 inference(resolution,[status(thm)],[f6095,f1264])).
% 208.68/41.84 fof(f11437,plain,(
% 208.68/41.84 ![X0,X1,X2]: (r1(X0)|~id(X1,sK1_skl(X0))|~sP9_prd(X1,X2))),
% 208.68/41.84 inference(resolution,[status(thm)],[f2126,f420])).
% 208.68/41.84 fof(f22674,plain,(
% 208.68/41.84 ![X0]: (r2(X0,sK20_skl(sK1_skl(X0)))|~r1(sK21_skl(sK1_skl(X0))))),
% 208.68/41.84 inference(resolution,[status(thm)],[f1753,f119])).
% 208.68/41.84 fof(f22675,plain,(
% 208.68/41.84 ![X0]: (r2(X0,sK20_skl(sK1_skl(X0))))),
% 208.68/41.84 inference(forward_subsumption_resolution,[status(thm)],[f22674,f573])).
% 208.68/41.84 fof(f23635,plain,(
% 208.68/41.84 ![X0]: (~r1(sK2_skl(sK13_skl(sK1_skl(X0)),sK1_skl(X0))))),
% 208.68/41.84 inference(resolution,[status(thm)],[f8501,f1883])).
% 208.68/41.84 fof(f24314,plain,(
% 208.68/41.84 ![X0,X1,X2]: (r1(X0)|~sP9_prd(X1,X2)|~r2(X0,X1))),
% 208.68/41.84 inference(resolution,[status(thm)],[f11437,f255])).
% 208.68/41.84 fof(f31631,plain,(
% 208.68/41.84 ![X0]: (r1(X0)|sP9_prd(sK20_skl(X0),sK20_skl(X0)))),
% 208.68/41.90 inference(resolution,[status(thm)],[f4705,f41])).
% 208.68/41.90 fof(f31639,plain,(
% 208.68/41.90 ![X0,X1]: (r1(X0)|r1(X1)|~r2(X1,sK20_skl(X0)))),
% 208.68/41.90 inference(resolution,[status(thm)],[f31631,f24314])).
% 208.68/41.90 fof(f31717,plain,(
% 208.68/41.90 ![X0]: (r1(sK1_skl(X0))|r1(X0))),
% 208.68/41.90 inference(resolution,[status(thm)],[f31639,f22675])).
% 208.68/41.90 fof(f31719,plain,(
% 208.68/41.90 ![X0]: (r1(X0))),
% 208.68/41.90 inference(forward_subsumption_resolution,[status(thm)],[f31717,f441])).
% 208.68/41.90 fof(f31876,plain,(
% 208.68/41.90 $false),
% 208.68/41.90 inference(backward_subsumption_resolution,[status(thm)],[f23635,f31719])).
% 208.68/41.90 % SZS output end CNFRefutation for theBenchmark.p
% 59.93/41.93 % Elapsed time: 26.503680 seconds
% 59.93/41.93 % CPU time: 209.501418 seconds
% 59.93/41.93 % Total memory used: 647.305 MB
% 59.93/41.93 % Net memory used: 504.535 MB
%------------------------------------------------------------------------------