%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM023+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 12:10:44 PM UTC 2026
% Result : Theorem 24.68s 3.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM023+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 14:18:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 24.68/3.55 % Refutation found
% 24.68/3.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 24.68/3.55 % SZS output start CNFRefutation for theBenchmark
% 24.68/3.55 fof(f17,hypothesis,(
% 24.68/3.55 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2)& ( W0 = W1| aReductOfIn0(W1,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W1) ))| sdtmndtplgtdt0(W0,xR,W1)| sdtmndtasgtdt0(W0,xR,W1) )& ( W0 = W2| aReductOfIn0(W2,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W2) ))| sdtmndtplgtdt0(W0,xR,W2)| sdtmndtasgtdt0(W0,xR,W2) ) )=> (? [W3] :( aElement0(W3)& ( W1 = W3| ( ( aReductOfIn0(W3,W1,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W1,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(W1,xR,W3) ) )& sdtmndtasgtdt0(W1,xR,W3)& ( W2 = W3| ( ( aReductOfIn0(W3,W2,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W2,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(W2,xR,W3) ) )& sdtmndtasgtdt0(W2,xR,W3) ) )) )),
% 24.68/3.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.68/3.55 fof(f18,conjecture,(
% 24.68/3.55 ( (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2)& ( W0 = W1| ( ( aReductOfIn0(W1,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W1) ) ))& sdtmndtplgtdt0(W0,xR,W1) ) )& sdtmndtasgtdt0(W0,xR,W1)& ( W0 = W2| ( ( aReductOfIn0(W2,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W2) ) ))& sdtmndtplgtdt0(W0,xR,W2) ) )& sdtmndtasgtdt0(W0,xR,W2) )=> (? [W3] :( aElement0(W3)& ( W1 = W3| aReductOfIn0(W3,W1,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W1,xR)& sdtmndtplgtdt0(W4,xR,W3) ))| sdtmndtplgtdt0(W1,xR,W3)| sdtmndtasgtdt0(W1,xR,W3) )& ( W2 = W3| aReductOfIn0(W3,W2,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W2,xR)& sdtmndtplgtdt0(W4,xR,W3) ))| sdtmndtplgtdt0(W2,xR,W3)| sdtmndtasgtdt0(W2,xR,W3) ) ) )))| isConfluent0(xR) ) ),
% 24.68/3.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 24.68/3.55 fof(f19,negated_conjecture,(
% 24.68/3.55 ~(( (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2)& ( W0 = W1| ( ( aReductOfIn0(W1,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W1) ) ))& sdtmndtplgtdt0(W0,xR,W1) ) )& sdtmndtasgtdt0(W0,xR,W1)& ( W0 = W2| ( ( aReductOfIn0(W2,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W2) ) ))& sdtmndtplgtdt0(W0,xR,W2) ) )& sdtmndtasgtdt0(W0,xR,W2) )=> (? [W3] :( aElement0(W3)& ( W1 = W3| aReductOfIn0(W3,W1,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W1,xR)& sdtmndtplgtdt0(W4,xR,W3) ))| sdtmndtplgtdt0(W1,xR,W3)| sdtmndtasgtdt0(W1,xR,W3) )& ( W2 = W3| aReductOfIn0(W3,W2,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W2,xR)& sdtmndtplgtdt0(W4,xR,W3) ))| sdtmndtplgtdt0(W2,xR,W3)| sdtmndtasgtdt0(W2,xR,W3) ) ) )))| isConfluent0(xR) ) )),
% 24.68/3.55 inference(negated_conjecture,[status(cth)],[f18])).
% 24.68/3.55 fof(f114,plain,(
% 24.68/3.55 ![W0,W1,W2]: (((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1)))|((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2)))|(?[W3]: ((((aElement0(W3)&(W1=W3|((aReductOfIn0(W3,W1,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W1,xR,W3))))&sdtmndtasgtdt0(W1,xR,W3))&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3))))),
% 24.68/3.55 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 24.68/3.55 fof(f115,definition,(
% 24.68/3.55 ![W0,W1]: (sP0_prd(W1,W0)<=>((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1)))),
% 24.68/3.55 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 24.68/3.55 fof(f116,definition,(
% 24.68/3.55 ![W0,W2]: (sP1_prd(W2,W0)<=>((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2)))),
% 24.68/3.55 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 24.68/3.55 fof(f117,plain,(
% 24.68/3.55 ![W0,W1,W2]: (((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sP0_prd(W1,W0))|sP1_prd(W2,W0))|(?[W3]: ((((aElement0(W3)&(W1=W3|((aReductOfIn0(W3,W1,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W1,xR,W3))))&sdtmndtasgtdt0(W1,xR,W3))&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3))))),
% 24.68/3.55 inference(formula_renaming,[status(thm)],[f114,f116,f115])).
% 24.68/3.55 fof(f118,plain,(
% 24.68/3.55 ![W1,W2]: ((![W0]: ((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sP0_prd(W1,W0))|sP1_prd(W2,W0)))|(?[W3]: ((((aElement0(W3)&(W1=W3|((aReductOfIn0(W3,W1,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W1,xR,W3))))&sdtmndtasgtdt0(W1,xR,W3))&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3))))),
% 24.68/3.55 inference(miniscoping,[status(thm)],[f117])).
% 24.68/3.55 fof(f119,plain,(
% 24.68/3.55 ![W1,W2]: ((![W0]: ((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sP0_prd(W1,W0))|sP1_prd(W2,W0)))|((((aElement0(sK16_skl(W2,W1))&(W1=sK16_skl(W2,W1)|((aReductOfIn0(sK16_skl(W2,W1),W1,xR)|((aElement0(sK17_skl(W2,W1))&aReductOfIn0(sK17_skl(W2,W1),W1,xR))&sdtmndtplgtdt0(sK17_skl(W2,W1),xR,sK16_skl(W2,W1))))&sdtmndtplgtdt0(W1,xR,sK16_skl(W2,W1)))))&sdtmndtasgtdt0(W1,xR,sK16_skl(W2,W1)))&(W2=sK16_skl(W2,W1)|((aReductOfIn0(sK16_skl(W2,W1),W2,xR)|((aElement0(sK18_skl(W2,W1))&aReductOfIn0(sK18_skl(W2,W1),W2,xR))&sdtmndtplgtdt0(sK18_skl(W2,W1),xR,sK16_skl(W2,W1))))&sdtmndtplgtdt0(W2,xR,sK16_skl(W2,W1)))))&sdtmndtasgtdt0(W2,xR,sK16_skl(W2,W1))))),
% 24.68/3.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(W3,sK16_skl(W2,W1)),skolemize(W4,sK17_skl(W2,W1)),skolemize(W4,sK18_skl(W2,W1))],[f118])).
% 24.68/3.55 fof(f120,plain,(
% 24.68/3.55 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|sP1_prd(X2,X0)|aElement0(sK16_skl(X2,X1)))),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f119])).
% 24.68/3.55 fof(f125,plain,(
% 24.68/3.55 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|sP1_prd(X2,X0)|sdtmndtasgtdt0(X1,xR,sK16_skl(X2,X1)))),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f119])).
% 24.68/3.55 fof(f130,plain,(
% 24.68/3.55 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|sP1_prd(X2,X0)|sdtmndtasgtdt0(X2,xR,sK16_skl(X2,X1)))),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f119])).
% 24.68/3.55 fof(f131,plain,(
% 24.68/3.55 ((?[W0,W1,W2]: (((((((aElement0(W0)&aElement0(W1))&aElement0(W2))&(W0=W1|((aReductOfIn0(W1,W0,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W1))))&sdtmndtplgtdt0(W0,xR,W1))))&sdtmndtasgtdt0(W0,xR,W1))&(W0=W2|((aReductOfIn0(W2,W0,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W0,xR,W2))))&sdtmndtasgtdt0(W0,xR,W2))&(![W3]: ((~aElement0(W3)|((((~W1=W3&~aReductOfIn0(W3,W1,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W1,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W1,xR,W3))&~sdtmndtasgtdt0(W1,xR,W3)))|((((~W2=W3&~aReductOfIn0(W3,W2,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W2,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W2,xR,W3))&~sdtmndtasgtdt0(W2,xR,W3))))))&~isConfluent0(xR))),
% 24.68/3.55 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 24.68/3.55 fof(f132,definition,(
% 24.68/3.55 ![W1,W3]: (sP2_prd(W3,W1)<=>((((~W1=W3&~aReductOfIn0(W3,W1,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W1,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W1,xR,W3))&~sdtmndtasgtdt0(W1,xR,W3)))),
% 24.68/3.55 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 24.68/3.55 fof(f133,plain,(
% 24.68/3.55 (?[W0,W1,W2]: (((((((aElement0(W0)&aElement0(W1))&aElement0(W2))&(W0=W1|((aReductOfIn0(W1,W0,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W1))))&sdtmndtplgtdt0(W0,xR,W1))))&sdtmndtasgtdt0(W0,xR,W1))&(W0=W2|((aReductOfIn0(W2,W0,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W0,xR,W2))))&sdtmndtasgtdt0(W0,xR,W2))&(![W3]: ((~aElement0(W3)|sP2_prd(W3,W1))|((((~W2=W3&~aReductOfIn0(W3,W2,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W2,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W2,xR,W3))&~sdtmndtasgtdt0(W2,xR,W3))))))&~isConfluent0(xR)),
% 24.68/3.55 inference(formula_renaming,[status(thm)],[f131,f132])).
% 24.68/3.55 fof(f134,plain,(
% 24.68/3.55 (?[W1,W2]: ((?[W0]: ((((((aElement0(W0)&aElement0(W1))&aElement0(W2))&(W0=W1|((aReductOfIn0(W1,W0,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W1))))&sdtmndtplgtdt0(W0,xR,W1))))&sdtmndtasgtdt0(W0,xR,W1))&(W0=W2|((aReductOfIn0(W2,W0,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W0,xR,W2))))&sdtmndtasgtdt0(W0,xR,W2)))&(![W3]: ((~aElement0(W3)|sP2_prd(W3,W1))|((((~W2=W3&~aReductOfIn0(W3,W2,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W2,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W2,xR,W3))&~sdtmndtasgtdt0(W2,xR,W3))))))&~isConfluent0(xR)),
% 24.68/3.55 inference(miniscoping,[status(thm)],[f133])).
% 24.68/3.55 fof(f135,plain,(
% 24.68/3.55 (((((((aElement0(sK21_skl)&aElement0(sK19_skl))&aElement0(sK20_skl))&(sK21_skl=sK19_skl|((aReductOfIn0(sK19_skl,sK21_skl,xR)|((aElement0(sK22_skl)&aReductOfIn0(sK22_skl,sK21_skl,xR))&sdtmndtplgtdt0(sK22_skl,xR,sK19_skl)))&sdtmndtplgtdt0(sK21_skl,xR,sK19_skl))))&sdtmndtasgtdt0(sK21_skl,xR,sK19_skl))&(sK21_skl=sK20_skl|((aReductOfIn0(sK20_skl,sK21_skl,xR)|((aElement0(sK23_skl)&aReductOfIn0(sK23_skl,sK21_skl,xR))&sdtmndtplgtdt0(sK23_skl,xR,sK20_skl)))&sdtmndtplgtdt0(sK21_skl,xR,sK20_skl))))&sdtmndtasgtdt0(sK21_skl,xR,sK20_skl))&(![W3]: ((~aElement0(W3)|sP2_prd(W3,sK19_skl))|((((~sK20_skl=W3&~aReductOfIn0(W3,sK20_skl,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,sK20_skl,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(sK20_skl,xR,W3))&~sdtmndtasgtdt0(sK20_skl,xR,W3)))))&~isConfluent0(xR)),
% 24.68/3.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl]),skolemize(W1,sK19_skl),skolemize(W2,sK20_skl),skolemize(W0,sK21_skl),skolemize(W3,sK22_skl),skolemize(W3,sK23_skl)],[f134])).
% 24.68/3.55 fof(f136,plain,(
% 24.68/3.55 aElement0(sK21_skl)),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f135])).
% 24.68/3.55 fof(f137,plain,(
% 24.68/3.55 aElement0(sK19_skl)),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f135])).
% 24.68/3.55 fof(f138,plain,(
% 24.68/3.55 aElement0(sK20_skl)),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f135])).
% 24.68/3.55 fof(f143,plain,(
% 24.68/3.55 sdtmndtasgtdt0(sK21_skl,xR,sK19_skl)),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f135])).
% 24.68/3.55 fof(f148,plain,(
% 24.68/3.55 sdtmndtasgtdt0(sK21_skl,xR,sK20_skl)),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f135])).
% 24.68/3.55 fof(f153,plain,(
% 24.68/3.55 ![X0]: (~aElement0(X0)|sP2_prd(X0,sK19_skl)|~sdtmndtasgtdt0(sK20_skl,xR,X0))),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f135])).
% 24.68/3.55 fof(f155,plain,(
% 24.68/3.55 ![W0,W1]: ((~sP0_prd(W1,W0)|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1)))&(sP0_prd(W1,W0)|((((W0=W1|aReductOfIn0(W1,W0,xR))|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W1))))|sdtmndtplgtdt0(W0,xR,W1))|sdtmndtasgtdt0(W0,xR,W1))))),
% 24.68/3.55 inference(NNF_transformation,[status(thm)],[f115])).
% 24.68/3.55 fof(f156,plain,(
% 24.68/3.55 (![W0,W1]: (~sP0_prd(W1,W0)|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1))))&(![W0,W1]: (sP0_prd(W1,W0)|((((W0=W1|aReductOfIn0(W1,W0,xR))|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W1))))|sdtmndtplgtdt0(W0,xR,W1))|sdtmndtasgtdt0(W0,xR,W1))))),
% 24.68/3.55 inference(miniscoping,[status(thm)],[f155])).
% 24.68/3.55 fof(f157,plain,(
% 24.68/3.55 (![W0,W1]: (~sP0_prd(W1,W0)|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1))))&(![W0,W1]: (sP0_prd(W1,W0)|((((W0=W1|aReductOfIn0(W1,W0,xR))|((aElement0(sK24_skl(W1,W0))&aReductOfIn0(sK24_skl(W1,W0),W0,xR))&sdtmndtplgtdt0(sK24_skl(W1,W0),xR,W1)))|sdtmndtplgtdt0(W0,xR,W1))|sdtmndtasgtdt0(W0,xR,W1))))),
% 24.68/3.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W3,sK24_skl(W1,W0))],[f156])).
% 24.68/3.55 fof(f162,plain,(
% 24.68/3.55 ![X0,X1]: (~sP0_prd(X0,X1)|~sdtmndtasgtdt0(X1,xR,X0))),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f157])).
% 24.68/3.55 fof(f166,plain,(
% 24.68/3.55 ![W0,W2]: ((~sP1_prd(W2,W0)|((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2)))&(sP1_prd(W2,W0)|((((W0=W2|aReductOfIn0(W2,W0,xR))|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))|sdtmndtplgtdt0(W0,xR,W2))|sdtmndtasgtdt0(W0,xR,W2))))),
% 24.68/3.55 inference(NNF_transformation,[status(thm)],[f116])).
% 24.68/3.55 fof(f167,plain,(
% 24.68/3.55 (![W0,W2]: (~sP1_prd(W2,W0)|((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2))))&(![W0,W2]: (sP1_prd(W2,W0)|((((W0=W2|aReductOfIn0(W2,W0,xR))|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))|sdtmndtplgtdt0(W0,xR,W2))|sdtmndtasgtdt0(W0,xR,W2))))),
% 24.68/3.55 inference(miniscoping,[status(thm)],[f166])).
% 24.68/3.55 fof(f168,plain,(
% 24.68/3.55 (![W0,W2]: (~sP1_prd(W2,W0)|((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2))))&(![W0,W2]: (sP1_prd(W2,W0)|((((W0=W2|aReductOfIn0(W2,W0,xR))|((aElement0(sK25_skl(W2,W0))&aReductOfIn0(sK25_skl(W2,W0),W0,xR))&sdtmndtplgtdt0(sK25_skl(W2,W0),xR,W2)))|sdtmndtplgtdt0(W0,xR,W2))|sdtmndtasgtdt0(W0,xR,W2))))),
% 24.68/3.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(W3,sK25_skl(W2,W0))],[f167])).
% 24.68/3.55 fof(f173,plain,(
% 24.68/3.55 ![X0,X1]: (~sP1_prd(X0,X1)|~sdtmndtasgtdt0(X1,xR,X0))),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f168])).
% 24.68/3.55 fof(f177,plain,(
% 24.68/3.55 ![W1,W3]: ((~sP2_prd(W3,W1)|((((~W1=W3&~aReductOfIn0(W3,W1,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W1,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W1,xR,W3))&~sdtmndtasgtdt0(W1,xR,W3)))&(sP2_prd(W3,W1)|((((W1=W3|aReductOfIn0(W3,W1,xR))|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))|sdtmndtplgtdt0(W1,xR,W3))|sdtmndtasgtdt0(W1,xR,W3))))),
% 24.68/3.55 inference(NNF_transformation,[status(thm)],[f132])).
% 24.68/3.55 fof(f178,plain,(
% 24.68/3.55 (![W1,W3]: (~sP2_prd(W3,W1)|((((~W1=W3&~aReductOfIn0(W3,W1,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W1,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W1,xR,W3))&~sdtmndtasgtdt0(W1,xR,W3))))&(![W1,W3]: (sP2_prd(W3,W1)|((((W1=W3|aReductOfIn0(W3,W1,xR))|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))|sdtmndtplgtdt0(W1,xR,W3))|sdtmndtasgtdt0(W1,xR,W3))))),
% 24.68/3.55 inference(miniscoping,[status(thm)],[f177])).
% 24.68/3.55 fof(f179,plain,(
% 24.68/3.55 (![W1,W3]: (~sP2_prd(W3,W1)|((((~W1=W3&~aReductOfIn0(W3,W1,xR))&(![W4]: ((~aElement0(W4)|~aReductOfIn0(W4,W1,xR))|~sdtmndtplgtdt0(W4,xR,W3))))&~sdtmndtplgtdt0(W1,xR,W3))&~sdtmndtasgtdt0(W1,xR,W3))))&(![W1,W3]: (sP2_prd(W3,W1)|((((W1=W3|aReductOfIn0(W3,W1,xR))|((aElement0(sK26_skl(W3,W1))&aReductOfIn0(sK26_skl(W3,W1),W1,xR))&sdtmndtplgtdt0(sK26_skl(W3,W1),xR,W3)))|sdtmndtplgtdt0(W1,xR,W3))|sdtmndtasgtdt0(W1,xR,W3))))),
% 24.68/3.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(W4,sK26_skl(W3,W1))],[f178])).
% 24.68/3.55 fof(f184,plain,(
% 24.68/3.55 ![X0,X1]: (~sP2_prd(X0,X1)|~sdtmndtasgtdt0(X1,xR,X0))),
% 24.68/3.55 inference(cnf_transformation,[status(thm)],[f179])).
% 24.68/3.55 fof(f230,plain,(
% 24.68/3.55 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(sK20_skl,X0)|sP1_prd(X1,X0)|aElement0(sK16_skl(X1,sK20_skl)))),
% 24.68/3.55 inference(resolution,[status(thm)],[f120,f138])).
% 24.68/3.55 fof(f322,plain,(
% 24.68/3.55 ![X0]: (~aElement0(X0)|sP0_prd(sK20_skl,X0)|sP1_prd(sK19_skl,X0)|aElement0(sK16_skl(sK19_skl,sK20_skl)))),
% 24.68/3.55 inference(resolution,[status(thm)],[f230,f137])).
% 24.68/3.55 fof(f339,plain,(
% 24.68/3.55 sP0_prd(sK20_skl,sK21_skl)|sP1_prd(sK19_skl,sK21_skl)|aElement0(sK16_skl(sK19_skl,sK20_skl))),
% 24.68/3.55 inference(resolution,[status(thm)],[f322,f136])).
% 24.68/3.55 fof(f1539,plain,(
% 24.68/3.55 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(X1,X0)|sP1_prd(sK19_skl,X0)|sdtmndtasgtdt0(X1,xR,sK16_skl(sK19_skl,X1)))),
% 24.68/3.56 inference(resolution,[status(thm)],[f125,f137])).
% 24.68/3.56 fof(f1718,plain,(
% 24.68/3.56 ![X0]: (~aElement0(X0)|sP0_prd(sK20_skl,X0)|sP1_prd(sK19_skl,X0)|sdtmndtasgtdt0(sK20_skl,xR,sK16_skl(sK19_skl,sK20_skl)))),
% 24.68/3.56 inference(resolution,[status(thm)],[f1539,f138])).
% 24.68/3.56 fof(f2410,plain,(
% 24.68/3.56 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(sK20_skl,X0)|sP1_prd(X1,X0)|sdtmndtasgtdt0(X1,xR,sK16_skl(X1,sK20_skl)))),
% 24.68/3.56 inference(resolution,[status(thm)],[f130,f138])).
% 24.68/3.56 fof(f2907,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)|sP1_prd(sK19_skl,sK21_skl)|sdtmndtasgtdt0(sK20_skl,xR,sK16_skl(sK19_skl,sK20_skl))),
% 24.68/3.56 inference(resolution,[status(thm)],[f1718,f136])).
% 24.68/3.56 fof(f3211,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)|sP1_prd(sK19_skl,sK21_skl)|~aElement0(sK16_skl(sK19_skl,sK20_skl))|sP2_prd(sK16_skl(sK19_skl,sK20_skl),sK19_skl)),
% 24.68/3.56 inference(resolution,[status(thm)],[f2907,f153])).
% 24.68/3.56 fof(f3212,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)|sP1_prd(sK19_skl,sK21_skl)|sP2_prd(sK16_skl(sK19_skl,sK20_skl),sK19_skl)),
% 24.68/3.56 inference(forward_subsumption_resolution,[status(thm)],[f3211,f339])).
% 24.68/3.56 fof(f3214,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)|sP1_prd(sK19_skl,sK21_skl)|~sdtmndtasgtdt0(sK19_skl,xR,sK16_skl(sK19_skl,sK20_skl))),
% 24.68/3.56 inference(resolution,[status(thm)],[f3212,f184])).
% 24.68/3.56 fof(f3633,plain,(
% 24.68/3.56 ![X0]: (~aElement0(X0)|sP0_prd(sK20_skl,X0)|sP1_prd(sK19_skl,X0)|sdtmndtasgtdt0(sK19_skl,xR,sK16_skl(sK19_skl,sK20_skl)))),
% 24.68/3.56 inference(resolution,[status(thm)],[f2410,f137])).
% 24.68/3.56 fof(f3742,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)|sP1_prd(sK19_skl,sK21_skl)|sdtmndtasgtdt0(sK19_skl,xR,sK16_skl(sK19_skl,sK20_skl))),
% 24.68/3.56 inference(resolution,[status(thm)],[f3633,f136])).
% 24.68/3.56 fof(f3746,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)|sP1_prd(sK19_skl,sK21_skl)),
% 24.68/3.56 inference(forward_subsumption_resolution,[status(thm)],[f3742,f3214])).
% 24.68/3.56 fof(f3747,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)|~sdtmndtasgtdt0(sK21_skl,xR,sK19_skl)),
% 24.68/3.56 inference(resolution,[status(thm)],[f3746,f173])).
% 24.68/3.56 fof(f3750,plain,(
% 24.68/3.56 sP0_prd(sK20_skl,sK21_skl)),
% 24.68/3.56 inference(forward_subsumption_resolution,[status(thm)],[f3747,f143])).
% 24.68/3.56 fof(f4321,plain,(
% 24.68/3.56 ~sdtmndtasgtdt0(sK21_skl,xR,sK20_skl)),
% 24.68/3.56 inference(resolution,[status(thm)],[f3750,f162])).
% 24.68/3.56 fof(f4322,plain,(
% 24.68/3.56 $false),
% 24.68/3.56 inference(forward_subsumption_resolution,[status(thm)],[f4321,f148])).
% 24.68/3.56 % SZS output end CNFRefutation for theBenchmark.p
% 24.68/3.59 % Elapsed time: 3.201713 seconds
% 24.68/3.59 % CPU time: 25.065643 seconds
% 24.68/3.59 % Total memory used: 242.151 MB
% 24.68/3.59 % Net memory used: 220.261 MB
%------------------------------------------------------------------------------