%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUN054+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:23 PM UTC 2026
% Result : Theorem 16.27s 2.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN054+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 03:25:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 16.27/2.49 % Refutation found
% 16.27/2.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.27/2.49 % SZS output start CNFRefutation for theBenchmark
% 16.27/2.49 fof(f1,axiom,(
% 16.27/2.49 (? [Y24] :(! [X19] :( ( id(X19,Y24)& r1(X19) )| ( ~ r1(X19)& ~ id(X19,Y24) ) ) ))),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f3,axiom,(
% 16.27/2.49 (! [X13,X14] :(? [Y22] :(! [X15] :( ( id(X15,Y22)& r3(X13,X14,X15) )| ( ~ r3(X13,X14,X15)& ~ id(X15,Y22) ) ) )))),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f5,axiom,(
% 16.27/2.49 (! [X20] : id(X20,X20) )),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f6,axiom,(
% 16.27/2.49 (! [X21,X22] :( ~ id(X21,X22)| id(X22,X21) ) )),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f7,axiom,(
% 16.27/2.49 (! [X23,X24,X25] :( ~ id(X23,X24)| id(X23,X25)| ~ id(X24,X25) ) )),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f8,axiom,(
% 16.27/2.49 (! [X26,X27] :( ~ id(X26,X27)| ( ~ r1(X26)& ~ r1(X27) )| ( r1(X26)& r1(X27) ) ) )),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f12,axiom,(
% 16.27/2.49 (! [X1,X8] :(? [Y4] :( (? [Y5] :( id(Y5,Y4)& (? [Y15] :( r2(X8,Y15)& r3(X1,Y15,Y5) ) )))& (? [Y7] :( r2(Y7,Y4)& r3(X1,X8,Y7) ) )) ))),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f15,axiom,(
% 16.27/2.49 (! [X4] :(? [Y9] :( id(Y9,X4)& (? [Y16] :( r1(Y16)& r3(X4,Y16,Y9) ) )) ))),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f19,conjecture,(
% 16.27/2.49 (? [Y1] :( (? [Y2] :( (? [Y4] :( r1(Y4)& r3(Y4,Y2,Y1) ))& (? [Y5] :( r1(Y5)& r2(Y5,Y2) ) )))& (? [Y3] :( id(Y1,Y3)& (? [Y6] :( r1(Y6)& r2(Y6,Y3) ) )) )) )),
% 16.27/2.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.27/2.49 fof(f20,negated_conjecture,(
% 16.27/2.49 ~((? [Y1] :( (? [Y2] :( (? [Y4] :( r1(Y4)& r3(Y4,Y2,Y1) ))& (? [Y5] :( r1(Y5)& r2(Y5,Y2) ) )))& (? [Y3] :( id(Y1,Y3)& (? [Y6] :( r1(Y6)& r2(Y6,Y3) ) )) )) ))),
% 16.27/2.49 inference(negated_conjecture,[status(cth)],[f19])).
% 16.27/2.49 fof(f21,definition,(
% 16.27/2.49 ![Y24,X19]: (sP0_prd(X19,Y24)<=>(id(X19,Y24)&r1(X19)))),
% 16.27/2.49 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 16.27/2.49 fof(f22,plain,(
% 16.27/2.49 ?[Y24]: ![X19]: (sP0_prd(X19,Y24)|(~r1(X19)&~id(X19,Y24)))),
% 16.27/2.49 inference(formula_renaming,[status(thm)],[f1,f21])).
% 16.27/2.49 fof(f23,plain,(
% 16.27/2.49 ![X19]: (sP0_prd(X19,sK0_skl)|(~r1(X19)&~id(X19,sK0_skl)))),
% 16.27/2.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y24,sK0_skl)],[f22])).
% 16.27/2.49 fof(f24,plain,(
% 16.27/2.49 ![X0]: (sP0_prd(X0,sK0_skl)|~r1(X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f23])).
% 16.27/2.49 fof(f25,plain,(
% 16.27/2.49 ![X0]: (sP0_prd(X0,sK0_skl)|~id(X0,sK0_skl))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f23])).
% 16.27/2.49 fof(f31,definition,(
% 16.27/2.49 ![X13,X14,Y22,X15]: (sP2_prd(X15,Y22,X14,X13)<=>(id(X15,Y22)&r3(X13,X14,X15)))),
% 16.27/2.49 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 16.27/2.49 fof(f32,plain,(
% 16.27/2.49 ![X13,X14]: ?[Y22]: ![X15]: (sP2_prd(X15,Y22,X14,X13)|(~r3(X13,X14,X15)&~id(X15,Y22)))),
% 16.27/2.49 inference(formula_renaming,[status(thm)],[f3,f31])).
% 16.27/2.49 fof(f33,plain,(
% 16.27/2.49 ![X13,X14]: ![X15]: (sP2_prd(X15,sK2_skl(X14,X13),X14,X13)|(~r3(X13,X14,X15)&~id(X15,sK2_skl(X14,X13))))),
% 16.27/2.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y22,sK2_skl(X14,X13))],[f32])).
% 16.27/2.49 fof(f34,plain,(
% 16.27/2.49 ![X0,X1,X2]: (sP2_prd(X0,sK2_skl(X1,X2),X1,X2)|~r3(X2,X1,X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f33])).
% 16.27/2.49 fof(f41,plain,(
% 16.27/2.49 ![X0]: (id(X0,X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f5])).
% 16.27/2.49 fof(f42,plain,(
% 16.27/2.49 ![X0,X1]: (~id(X0,X1)|id(X1,X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f6])).
% 16.27/2.49 fof(f43,plain,(
% 16.27/2.49 ![X24,X25]: ((![X23]: (~id(X23,X24)|id(X23,X25)))|~id(X24,X25))),
% 16.27/2.49 inference(miniscoping,[status(thm)],[f7])).
% 16.27/2.49 fof(f44,plain,(
% 16.27/2.49 ![X0,X1,X2]: (~id(X0,X1)|id(X0,X2)|~id(X1,X2))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f43])).
% 16.27/2.49 fof(f45,definition,(
% 16.27/2.49 ![X26,X27]: (sP4_prd(X27,X26)<=>(~r1(X26)&~r1(X27)))),
% 16.27/2.49 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 16.27/2.49 fof(f46,plain,(
% 16.27/2.49 ![X26,X27]: ((~id(X26,X27)|sP4_prd(X27,X26))|(r1(X26)&r1(X27)))),
% 16.27/2.49 inference(formula_renaming,[status(thm)],[f8,f45])).
% 16.27/2.49 fof(f47,plain,(
% 16.27/2.49 ![X0,X1]: (~id(X0,X1)|sP4_prd(X1,X0)|r1(X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f46])).
% 16.27/2.49 fof(f48,plain,(
% 16.27/2.49 ![X0,X1]: (~id(X0,X1)|sP4_prd(X1,X0)|r1(X1))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f46])).
% 16.27/2.49 fof(f61,plain,(
% 16.27/2.49 ![X1,X8]: ((id(sK5_skl(X8,X1),sK4_skl(X8,X1))&(r2(X8,sK6_skl(X8,X1))&r3(X1,sK6_skl(X8,X1),sK5_skl(X8,X1))))&(r2(sK7_skl(X8,X1),sK4_skl(X8,X1))&r3(X1,X8,sK7_skl(X8,X1))))),
% 16.27/2.49 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))],[f12])).
% 16.27/2.49 fof(f62,plain,(
% 16.27/2.49 ![X0,X1]: (id(sK5_skl(X0,X1),sK4_skl(X0,X1)))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f61])).
% 16.27/2.49 fof(f63,plain,(
% 16.27/2.49 ![X0,X1]: (r2(X0,sK6_skl(X0,X1)))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f61])).
% 16.27/2.49 fof(f64,plain,(
% 16.27/2.49 ![X0,X1]: (r3(X0,sK6_skl(X1,X0),sK5_skl(X1,X0)))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f61])).
% 16.27/2.49 fof(f65,plain,(
% 16.27/2.49 ![X0,X1]: (r2(sK7_skl(X0,X1),sK4_skl(X0,X1)))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f61])).
% 16.27/2.49 fof(f66,plain,(
% 16.27/2.49 ![X0,X1]: (r3(X0,X1,sK7_skl(X1,X0)))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f61])).
% 16.27/2.49 fof(f74,plain,(
% 16.27/2.49 ![X4]: (id(sK12_skl(X4),X4)&(r1(sK13_skl(X4))&r3(X4,sK13_skl(X4),sK12_skl(X4))))),
% 16.27/2.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(Y9,sK12_skl(X4)),skolemize(Y16,sK13_skl(X4))],[f15])).
% 16.27/2.49 fof(f75,plain,(
% 16.27/2.49 ![X0]: (id(sK12_skl(X0),X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f74])).
% 16.27/2.49 fof(f76,plain,(
% 16.27/2.49 ![X0]: (r1(sK13_skl(X0)))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f74])).
% 16.27/2.49 fof(f77,plain,(
% 16.27/2.49 ![X0]: (r3(X0,sK13_skl(X0),sK12_skl(X0)))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f74])).
% 16.27/2.49 fof(f91,plain,(
% 16.27/2.49 (![Y1]: ((![Y2]: ((![Y4]: (~r1(Y4)|~r3(Y4,Y2,Y1)))|(![Y5]: (~r1(Y5)|~r2(Y5,Y2)))))|(![Y3]: (~id(Y1,Y3)|(![Y6]: (~r1(Y6)|~r2(Y6,Y3)))))))),
% 16.27/2.49 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 16.27/2.49 fof(f92,plain,(
% 16.27/2.49 ![X0,X1,X2,X3,X4,X5]: (~r1(X0)|~r3(X0,X1,X2)|~r1(X3)|~r2(X3,X1)|~id(X2,X4)|~r1(X5)|~r2(X5,X4))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f91])).
% 16.27/2.49 fof(f93,plain,(
% 16.27/2.49 ![Y24,X19]: ((~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19)))&(sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 16.27/2.49 inference(NNF_transformation,[status(thm)],[f21])).
% 16.27/2.49 fof(f94,plain,(
% 16.27/2.49 (![Y24,X19]: (~sP0_prd(X19,Y24)|(id(X19,Y24)&r1(X19))))&(![Y24,X19]: (sP0_prd(X19,Y24)|(~id(X19,Y24)|~r1(X19))))),
% 16.27/2.49 inference(miniscoping,[status(thm)],[f93])).
% 16.27/2.49 fof(f95,plain,(
% 16.27/2.49 ![X0,X1]: (~sP0_prd(X0,X1)|id(X0,X1))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f94])).
% 16.27/2.49 fof(f96,plain,(
% 16.27/2.49 ![X0,X1]: (~sP0_prd(X0,X1)|r1(X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f94])).
% 16.27/2.49 fof(f103,plain,(
% 16.27/2.49 ![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))))),
% 16.27/2.49 inference(NNF_transformation,[status(thm)],[f31])).
% 16.27/2.49 fof(f104,plain,(
% 16.27/2.49 (![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))))),
% 16.27/2.49 inference(miniscoping,[status(thm)],[f103])).
% 16.27/2.49 fof(f105,plain,(
% 16.27/2.49 ![X0,X1,X2,X3]: (~sP2_prd(X0,X1,X2,X3)|id(X0,X1))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f104])).
% 16.27/2.49 fof(f113,plain,(
% 16.27/2.49 ![X26,X27]: ((~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27)))&(sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 16.27/2.49 inference(NNF_transformation,[status(thm)],[f45])).
% 16.27/2.49 fof(f114,plain,(
% 16.27/2.49 (![X26,X27]: (~sP4_prd(X27,X26)|(~r1(X26)&~r1(X27))))&(![X26,X27]: (sP4_prd(X27,X26)|(r1(X26)|r1(X27))))),
% 16.27/2.49 inference(miniscoping,[status(thm)],[f113])).
% 16.27/2.49 fof(f115,plain,(
% 16.27/2.49 ![X0,X1]: (~sP4_prd(X0,X1)|~r1(X1))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f114])).
% 16.27/2.49 fof(f116,plain,(
% 16.27/2.49 ![X0,X1]: (~sP4_prd(X0,X1)|~r1(X0))),
% 16.27/2.49 inference(cnf_transformation,[status(thm)],[f114])).
% 16.27/2.49 fof(f164,plain,(
% 16.27/2.49 sP0_prd(sK12_skl(sK0_skl),sK0_skl)),
% 16.27/2.49 inference(resolution,[status(thm)],[f25,f75])).
% 16.27/2.49 fof(f167,plain,(
% 16.27/2.49 sP0_prd(sK0_skl,sK0_skl)),
% 16.27/2.49 inference(resolution,[status(thm)],[f25,f41])).
% 16.27/2.49 fof(f168,plain,(
% 16.27/2.49 r1(sK0_skl)),
% 16.27/2.49 inference(resolution,[status(thm)],[f167,f96])).
% 16.27/2.49 fof(f189,plain,(
% 16.27/2.49 ![X0]: (id(X0,sK0_skl)|~r1(X0))),
% 16.27/2.49 inference(resolution,[status(thm)],[f95,f24])).
% 16.27/2.49 fof(f191,plain,(
% 16.27/2.49 r1(sK12_skl(sK0_skl))),
% 16.27/2.49 inference(resolution,[status(thm)],[f164,f96])).
% 16.27/2.49 fof(f243,plain,(
% 16.27/2.49 ![X0,X1,X2]: (sP4_prd(X0,X1)|r1(X1)|~id(X1,X2)|~id(X2,X0))),
% 16.27/2.49 inference(resolution,[status(thm)],[f47,f44])).
% 16.27/2.49 fof(f269,definition,(
% 16.27/2.49 sQ1_spl <=> (r1(sK0_skl))),
% 16.27/2.49 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 16.27/2.49 fof(f300,plain,(
% 16.27/2.49 ![X0]: (sP4_prd(sK0_skl,X0)|r1(sK0_skl)|~r1(X0))),
% 16.27/2.49 inference(resolution,[status(thm)],[f48,f189])).
% 16.27/2.49 fof(f302,plain,(
% 16.27/2.49 ![X0,X1]: (sP4_prd(X0,X1)|r1(X0)|~id(X0,X1))),
% 16.27/2.49 inference(resolution,[status(thm)],[f48,f42])).
% 16.27/2.49 fof(f305,definition,(
% 16.27/2.49 ![X0]: (sQ2_spl <=> (sP4_prd(sK0_skl,X0)|~r1(X0)))),
% 16.27/2.49 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 16.27/2.49 fof(f306,plain,(
% 16.27/2.49 ![X0]: (sP4_prd(sK0_skl,X0)|~r1(X0)|~sQ2_spl)),
% 16.27/2.49 inference(component_clause,[status(thm)],[f305])).
% 16.27/2.49 fof(f308,plain,(
% 16.27/2.49 sQ2_spl|sQ1_spl),
% 16.27/2.49 inference(split_clause,[status(thm)],[f300,f305,f269])).
% 16.27/2.49 fof(f309,plain,(
% 16.27/2.49 ![X0]: (~r1(X0)|~sQ2_spl)),
% 16.27/2.49 inference(forward_subsumption_resolution,[status(thm)],[f306,f115])).
% 16.27/2.49 fof(f339,plain,(
% 16.27/2.49 $false|~sQ2_spl),
% 16.27/2.49 inference(backward_subsumption_resolution,[status(thm)],[f191,f309])).
% 16.27/2.49 fof(f344,plain,(
% 16.27/2.49 ~sQ2_spl),
% 16.27/2.49 inference(contradiction_clause,[status(thm)],[f339])).
% 16.27/2.49 fof(f403,plain,(
% 16.27/2.49 ![X0,X1,X2,X3,X4]: (~r1(X0)|~r1(X1)|~r2(X1,sK6_skl(X2,X0))|~id(sK5_skl(X2,X0),X3)|~r1(X4)|~r2(X4,X3))),
% 16.27/2.49 inference(resolution,[status(thm)],[f64,f92])).
% 16.27/2.49 fof(f428,plain,(
% 16.27/2.49 ![X0,X1,X2]: (r1(X0)|~id(X0,X1)|~id(X1,X2)|~r1(X2))),
% 16.27/2.49 inference(resolution,[status(thm)],[f243,f116])).
% 16.27/2.49 fof(f443,plain,(
% 16.27/2.49 ![X0,X1,X2]: (id(X0,sK2_skl(X1,X2))|~r3(X2,X1,X0))),
% 16.27/2.49 inference(resolution,[status(thm)],[f105,f34])).
% 16.27/2.49 fof(f961,plain,(
% 16.27/2.49 ![X0,X1,X2,X3]: (~r1(X0)|~r1(X1)|~id(sK5_skl(X1,X0),X2)|~r1(X3)|~r2(X3,X2))),
% 16.27/2.49 inference(resolution,[status(thm)],[f403,f63])).
% 16.27/2.49 fof(f2055,plain,(
% 16.27/2.49 ![X0]: (id(sK12_skl(X0),sK2_skl(sK13_skl(X0),X0)))),
% 16.27/2.49 inference(resolution,[status(thm)],[f443,f77])).
% 16.27/2.49 fof(f2056,plain,(
% 16.27/2.49 ![X0,X1]: (id(sK7_skl(X0,X1),sK2_skl(X0,X1)))),
% 16.27/2.49 inference(resolution,[status(thm)],[f443,f66])).
% 16.27/2.49 fof(f2171,plain,(
% 16.27/2.49 ![X0,X1]: (sP4_prd(sK7_skl(X0,X1),sK2_skl(X0,X1))|r1(sK7_skl(X0,X1)))),
% 16.27/2.49 inference(resolution,[status(thm)],[f2056,f302])).
% 16.27/2.49 fof(f2975,plain,(
% 16.27/2.49 ![X0,X1]: (r1(X0)|~id(X0,X1)|~id(X1,sK0_skl))),
% 16.27/2.49 inference(resolution,[status(thm)],[f428,f168])).
% 16.27/2.49 fof(f3944,plain,(
% 16.27/2.49 ![X0,X1,X2]: (~r1(X0)|~r1(X1)|~r1(X2)|~r2(X2,sK4_skl(X1,X0)))),
% 16.27/2.49 inference(resolution,[status(thm)],[f961,f62])).
% 16.27/2.49 fof(f5161,plain,(
% 16.27/2.49 ![X0,X1]: (~r1(X0)|~r1(X1)|~r1(sK7_skl(X1,X0)))),
% 16.27/2.49 inference(resolution,[status(thm)],[f3944,f65])).
% 16.27/2.49 fof(f5321,plain,(
% 16.27/2.49 ![X0]: (r1(X0)|~id(X0,sK12_skl(sK0_skl)))),
% 16.27/2.49 inference(resolution,[status(thm)],[f2975,f75])).
% 16.27/2.49 fof(f5505,plain,(
% 16.27/2.49 ![X0]: (r1(X0)|~id(sK12_skl(sK0_skl),X0))),
% 16.27/2.49 inference(resolution,[status(thm)],[f5321,f42])).
% 16.27/2.49 fof(f5521,plain,(
% 16.27/2.49 r1(sK2_skl(sK13_skl(sK0_skl),sK0_skl))),
% 16.27/2.49 inference(resolution,[status(thm)],[f5505,f2055])).
% 16.27/2.49 fof(f9550,plain,(
% 16.27/2.49 ![X0,X1]: (r1(sK7_skl(X0,X1))|~r1(sK2_skl(X0,X1)))),
% 16.27/2.49 inference(resolution,[status(thm)],[f2171,f115])).
% 16.27/2.49 fof(f10240,plain,(
% 16.27/2.49 r1(sK7_skl(sK13_skl(sK0_skl),sK0_skl))),
% 16.27/2.49 inference(resolution,[status(thm)],[f9550,f5521])).
% 16.27/2.49 fof(f10243,plain,(
% 16.27/2.49 ~r1(sK0_skl)|~r1(sK13_skl(sK0_skl))),
% 16.27/2.49 inference(resolution,[status(thm)],[f10240,f5161])).
% 16.27/2.49 fof(f10250,definition,(
% 16.27/2.49 sQ395_spl <=> (r1(sK13_skl(sK0_skl)))),
% 16.27/2.49 introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition])).
% 16.27/2.49 fof(f10252,plain,(
% 16.27/2.49 ~r1(sK13_skl(sK0_skl))|sQ395_spl),
% 16.27/2.49 inference(component_clause,[status(thm)],[f10250])).
% 16.27/2.49 fof(f10253,plain,(
% 16.27/2.49 ~sQ1_spl|~sQ395_spl),
% 16.27/2.49 inference(split_clause,[status(thm)],[f10243,f269,f10250])).
% 16.27/2.49 fof(f10254,plain,(
% 16.27/2.49 $false|sQ395_spl),
% 16.27/2.49 inference(forward_subsumption_resolution,[status(thm)],[f10252,f76])).
% 16.27/2.49 fof(f10255,plain,(
% 16.27/2.49 sQ395_spl),
% 16.27/2.49 inference(contradiction_clause,[status(thm)],[f10254])).
% 16.27/2.49 fof(f10256,plain,(
% 16.27/2.49 $false),
% 16.27/2.49 inference(sat_refutation,[status(thm)],[f308,f344,f10253,f10255])).
% 16.27/2.49 % SZS output end CNFRefutation for theBenchmark.p
% 16.27/2.52 % Elapsed time: 2.156048 seconds
% 16.27/2.52 % CPU time: 16.857810 seconds
% 16.27/2.52 % Total memory used: 130.328 MB
% 16.27/2.52 % Net memory used: 98.964 MB
%------------------------------------------------------------------------------