%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM022+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 0.12s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM022+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n011.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 14:15:25 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.40 fof(f17,hypothesis,(
% 0.12/0.40 ( aElement0(xa)& aElement0(xb)& aElement0(xc) ) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f19,conjecture,(
% 0.12/0.40 ( ( ( ( aReductOfIn0(xb,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xb) ))| sdtmndtplgtdt0(xa,xR,xb) )& ( aReductOfIn0(xc,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xc) ))| sdtmndtplgtdt0(xa,xR,xc) ) )=> (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& ( W0 = xb| ( ( aReductOfIn0(xb,W0,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,W0,xR)& sdtmndtplgtdt0(W1,xR,xb) ) ))& sdtmndtplgtdt0(W0,xR,xb) ) )& sdtmndtasgtdt0(W0,xR,xb)& (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xa,xR)& ( W1 = xc| ( ( aReductOfIn0(xc,W1,xR)| (? [W2] :( aElement0(W2)& aReductOfIn0(W2,W1,xR)& sdtmndtplgtdt0(W2,xR,xc) ) ))& sdtmndtplgtdt0(W1,xR,xc) ) )& sdtmndtasgtdt0(W1,xR,xc)& (? [W2] :( aElement0(W2)& ( 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)& ( W1 = W2| ( ( aReductOfIn0(W2,W1,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W1,xR)& sdtmndtplgtdt0(W3,xR,W2) ) ))& sdtmndtplgtdt0(W1,xR,W2) ) )& sdtmndtasgtdt0(W1,xR,W2)& (? [W3] :( aElement0(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)& ~ (? [W4] : aReductOfIn0(W4,W3,xR))& aNormalFormOfIn0(W3,W2,xR)& ( xb = W3| ( ( aReductOfIn0(W3,xb,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,xb,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(xb,xR,W3) ) )& sdtmndtasgtdt0(xb,xR,W3)& ( xc = W3| ( ( aReductOfIn0(W3,xc,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,xc,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(xc,xR,W3) ) )& sdtmndtasgtdt0(xc,xR,W3) ) )) )) )) ))=> ( ( ( xa = xb| ( ( aReductOfIn0(xb,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xb) ) ))& sdtmndtplgtdt0(xa,xR,xb) ) )& sdtmndtasgtdt0(xa,xR,xb)& ( xa = xc| ( ( aReductOfIn0(xc,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xc) ) ))& sdtmndtplgtdt0(xa,xR,xc) ) )& sdtmndtasgtdt0(xa,xR,xc) )=> (? [W0] :( aElement0(W0)& ( xb = W0| aReductOfIn0(W0,xb,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xb,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xb,xR,W0)| sdtmndtasgtdt0(xb,xR,W0) )& ( xc = W0| aReductOfIn0(W0,xc,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xc,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xc,xR,W0)| sdtmndtasgtdt0(xc,xR,W0) ) ) )) ) ),
% 0.12/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f20,negated_conjecture,(
% 0.12/0.40 ~(( ( ( ( aReductOfIn0(xb,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xb) ))| sdtmndtplgtdt0(xa,xR,xb) )& ( aReductOfIn0(xc,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xc) ))| sdtmndtplgtdt0(xa,xR,xc) ) )=> (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& ( W0 = xb| ( ( aReductOfIn0(xb,W0,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,W0,xR)& sdtmndtplgtdt0(W1,xR,xb) ) ))& sdtmndtplgtdt0(W0,xR,xb) ) )& sdtmndtasgtdt0(W0,xR,xb)& (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xa,xR)& ( W1 = xc| ( ( aReductOfIn0(xc,W1,xR)| (? [W2] :( aElement0(W2)& aReductOfIn0(W2,W1,xR)& sdtmndtplgtdt0(W2,xR,xc) ) ))& sdtmndtplgtdt0(W1,xR,xc) ) )& sdtmndtasgtdt0(W1,xR,xc)& (? [W2] :( aElement0(W2)& ( 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)& ( W1 = W2| ( ( aReductOfIn0(W2,W1,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W1,xR)& sdtmndtplgtdt0(W3,xR,W2) ) ))& sdtmndtplgtdt0(W1,xR,W2) ) )& sdtmndtasgtdt0(W1,xR,W2)& (? [W3] :( aElement0(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)& ~ (? [W4] : aReductOfIn0(W4,W3,xR))& aNormalFormOfIn0(W3,W2,xR)& ( xb = W3| ( ( aReductOfIn0(W3,xb,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,xb,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(xb,xR,W3) ) )& sdtmndtasgtdt0(xb,xR,W3)& ( xc = W3| ( ( aReductOfIn0(W3,xc,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,xc,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(xc,xR,W3) ) )& sdtmndtasgtdt0(xc,xR,W3) ) )) )) )) ))=> ( ( ( xa = xb| ( ( aReductOfIn0(xb,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xb) ) ))& sdtmndtplgtdt0(xa,xR,xb) ) )& sdtmndtasgtdt0(xa,xR,xb)& ( xa = xc| ( ( aReductOfIn0(xc,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xc) ) ))& sdtmndtplgtdt0(xa,xR,xc) ) )& sdtmndtasgtdt0(xa,xR,xc) )=> (? [W0] :( aElement0(W0)& ( xb = W0| aReductOfIn0(W0,xb,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xb,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xb,xR,W0)| sdtmndtasgtdt0(xb,xR,W0) )& ( xc = W0| aReductOfIn0(W0,xc,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xc,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xc,xR,W0)| sdtmndtasgtdt0(xc,xR,W0) ) ) )) ) )),
% 0.12/0.40 inference(negated_conjecture,[status(cth)],[f19])).
% 0.12/0.40 fof(f116,plain,(
% 0.12/0.40 aElement0(xb)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.40 fof(f117,plain,(
% 0.12/0.40 aElement0(xc)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.40 fof(f177,plain,(
% 0.12/0.40 (((((~aReductOfIn0(xb,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb))|((~aReductOfIn0(xc,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc)))|(?[W0]: ((((aElement0(W0)&aReductOfIn0(W0,xa,xR))&(W0=xb|((aReductOfIn0(xb,W0,xR)|(?[W1]: ((aElement0(W1)&aReductOfIn0(W1,W0,xR))&sdtmndtplgtdt0(W1,xR,xb))))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]: ((((aElement0(W1)&aReductOfIn0(W1,xa,xR))&(W1=xc|((aReductOfIn0(xc,W1,xR)|(?[W2]: ((aElement0(W2)&aReductOfIn0(W2,W1,xR))&sdtmndtplgtdt0(W2,xR,xc))))&sdtmndtplgtdt0(W1,xR,xc))))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]: (((((aElement0(W2)&(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))&(W1=W2|((aReductOfIn0(W2,W1,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W1,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W1,xR,W2))))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]: ((((((((aElement0(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))&(![W4]: ~aReductOfIn0(W4,W3,xR)))&aNormalFormOfIn0(W3,W2,xR))&(xb=W3|((aReductOfIn0(W3,xb,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,xb,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xb,xR,W3))))&sdtmndtasgtdt0(xb,xR,W3))&(xc=W3|((aReductOfIn0(W3,xc,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,xc,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xc,xR,W3))))&sdtmndtasgtdt0(xc,xR,W3))))))))))&(((((xa=xb|((aReductOfIn0(xb,xa,xR)|(?[W0]: ((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|(?[W0]: ((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&(![W0]: ((~aElement0(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0)))|((((~xc=W0&~aReductOfIn0(W0,xc,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xc,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xc,xR,W0))&~sdtmndtasgtdt0(xc,xR,W0))))))),
% 0.12/0.40 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.12/0.40 fof(f178,definition,(
% 0.12/0.40 sP1_prd<=>(((~aReductOfIn0(xb,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb))|((~aReductOfIn0(xc,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc)))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.12/0.40 fof(f179,definition,(
% 0.12/0.40 ![W0]: (sP2_prd(W0)<=>((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0)))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.12/0.40 fof(f180,plain,(
% 0.12/0.40 (sP1_prd|(?[W0]: ((((aElement0(W0)&aReductOfIn0(W0,xa,xR))&(W0=xb|((aReductOfIn0(xb,W0,xR)|(?[W1]: ((aElement0(W1)&aReductOfIn0(W1,W0,xR))&sdtmndtplgtdt0(W1,xR,xb))))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]: ((((aElement0(W1)&aReductOfIn0(W1,xa,xR))&(W1=xc|((aReductOfIn0(xc,W1,xR)|(?[W2]: ((aElement0(W2)&aReductOfIn0(W2,W1,xR))&sdtmndtplgtdt0(W2,xR,xc))))&sdtmndtplgtdt0(W1,xR,xc))))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]: (((((aElement0(W2)&(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))&(W1=W2|((aReductOfIn0(W2,W1,xR)|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W1,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W1,xR,W2))))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]: ((((((((aElement0(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))&(![W4]: ~aReductOfIn0(W4,W3,xR)))&aNormalFormOfIn0(W3,W2,xR))&(xb=W3|((aReductOfIn0(W3,xb,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,xb,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xb,xR,W3))))&sdtmndtasgtdt0(xb,xR,W3))&(xc=W3|((aReductOfIn0(W3,xc,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,xc,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xc,xR,W3))))&sdtmndtasgtdt0(xc,xR,W3))))))))))&(((((xa=xb|((aReductOfIn0(xb,xa,xR)|(?[W0]: ((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|(?[W0]: ((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&(![W0]: ((~aElement0(W0)|sP2_prd(W0))|((((~xc=W0&~aReductOfIn0(W0,xc,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xc,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xc,xR,W0))&~sdtmndtasgtdt0(xc,xR,W0)))))),
% 0.12/0.40 inference(formula_renaming,[status(thm)],[f177,f179,f178])).
% 0.12/0.40 fof(f181,plain,(
% 0.12/0.40 (sP1_prd|((((aElement0(sK19_skl)&aReductOfIn0(sK19_skl,xa,xR))&(sK19_skl=xb|((aReductOfIn0(xb,sK19_skl,xR)|((aElement0(sK20_skl)&aReductOfIn0(sK20_skl,sK19_skl,xR))&sdtmndtplgtdt0(sK20_skl,xR,xb)))&sdtmndtplgtdt0(sK19_skl,xR,xb))))&sdtmndtasgtdt0(sK19_skl,xR,xb))&((((aElement0(sK21_skl)&aReductOfIn0(sK21_skl,xa,xR))&(sK21_skl=xc|((aReductOfIn0(xc,sK21_skl,xR)|((aElement0(sK22_skl)&aReductOfIn0(sK22_skl,sK21_skl,xR))&sdtmndtplgtdt0(sK22_skl,xR,xc)))&sdtmndtplgtdt0(sK21_skl,xR,xc))))&sdtmndtasgtdt0(sK21_skl,xR,xc))&(((((aElement0(sK23_skl)&(sK19_skl=sK23_skl|((aReductOfIn0(sK23_skl,sK19_skl,xR)|((aElement0(sK24_skl)&aReductOfIn0(sK24_skl,sK19_skl,xR))&sdtmndtplgtdt0(sK24_skl,xR,sK23_skl)))&sdtmndtplgtdt0(sK19_skl,xR,sK23_skl))))&sdtmndtasgtdt0(sK19_skl,xR,sK23_skl))&(sK21_skl=sK23_skl|((aReductOfIn0(sK23_skl,sK21_skl,xR)|((aElement0(sK25_skl)&aReductOfIn0(sK25_skl,sK21_skl,xR))&sdtmndtplgtdt0(sK25_skl,xR,sK23_skl)))&sdtmndtplgtdt0(sK21_skl,xR,sK23_skl))))&sdtmndtasgtdt0(sK21_skl,xR,sK23_skl))&((((((((aElement0(sK26_skl)&(sK23_skl=sK26_skl|((aReductOfIn0(sK26_skl,sK23_skl,xR)|((aElement0(sK27_skl)&aReductOfIn0(sK27_skl,sK23_skl,xR))&sdtmndtplgtdt0(sK27_skl,xR,sK26_skl)))&sdtmndtplgtdt0(sK23_skl,xR,sK26_skl))))&sdtmndtasgtdt0(sK23_skl,xR,sK26_skl))&(![W4]: ~aReductOfIn0(W4,sK26_skl,xR)))&aNormalFormOfIn0(sK26_skl,sK23_skl,xR))&(xb=sK26_skl|((aReductOfIn0(sK26_skl,xb,xR)|((aElement0(sK28_skl)&aReductOfIn0(sK28_skl,xb,xR))&sdtmndtplgtdt0(sK28_skl,xR,sK26_skl)))&sdtmndtplgtdt0(xb,xR,sK26_skl))))&sdtmndtasgtdt0(xb,xR,sK26_skl))&(xc=sK26_skl|((aReductOfIn0(sK26_skl,xc,xR)|((aElement0(sK29_skl)&aReductOfIn0(sK29_skl,xc,xR))&sdtmndtplgtdt0(sK29_skl,xR,sK26_skl)))&sdtmndtplgtdt0(xc,xR,sK26_skl))))&sdtmndtasgtdt0(xc,xR,sK26_skl))))))&(((((xa=xb|((aReductOfIn0(xb,xa,xR)|((aElement0(sK30_skl)&aReductOfIn0(sK30_skl,xa,xR))&sdtmndtplgtdt0(sK30_skl,xR,xb)))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|((aElement0(sK31_skl)&aReductOfIn0(sK31_skl,xa,xR))&sdtmndtplgtdt0(sK31_skl,xR,xc)))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&(![W0]: ((~aElement0(W0)|sP2_prd(W0))|((((~xc=W0&~aReductOfIn0(W0,xc,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xc,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xc,xR,W0))&~sdtmndtasgtdt0(xc,xR,W0)))))),
% 0.12/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl,sK31_skl]),skolemize(W0,sK19_skl),skolemize(W1,sK20_skl),skolemize(W1,sK21_skl),skolemize(W2,sK22_skl),skolemize(W2,sK23_skl),skolemize(W3,sK24_skl),skolemize(W3,sK25_skl),skolemize(W3,sK26_skl),skolemize(W4,sK27_skl),skolemize(W4,sK28_skl),skolemize(W4,sK29_skl),skolemize(W0,sK30_skl),skolemize(W0,sK31_skl)],[f180])).
% 0.12/0.40 fof(f207,plain,(
% 0.12/0.40 sP1_prd|aElement0(sK26_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f219,plain,(
% 0.12/0.40 sP1_prd|sdtmndtasgtdt0(xb,xR,sK26_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f224,plain,(
% 0.12/0.40 sP1_prd|sdtmndtasgtdt0(xc,xR,sK26_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f228,plain,(
% 0.12/0.40 xa=xb|sdtmndtplgtdt0(xa,xR,xb)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f229,plain,(
% 0.12/0.40 sdtmndtasgtdt0(xa,xR,xb)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f233,plain,(
% 0.12/0.40 xa=xc|sdtmndtplgtdt0(xa,xR,xc)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f235,plain,(
% 0.12/0.40 ![X0]: (~aElement0(X0)|sP2_prd(X0)|~xc=X0)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f239,plain,(
% 0.12/0.40 ![X0]: (~aElement0(X0)|sP2_prd(X0)|~sdtmndtasgtdt0(xc,xR,X0))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f181])).
% 0.12/0.40 fof(f251,definition,(
% 0.12/0.40 sP3_prd<=>((~aReductOfIn0(xb,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.12/0.40 fof(f252,plain,(
% 0.12/0.40 sP1_prd<=>(sP3_prd|((~aReductOfIn0(xc,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc)))),
% 0.12/0.40 inference(formula_renaming,[status(thm)],[f178,f251])).
% 0.12/0.40 fof(f253,plain,(
% 0.12/0.40 (~sP1_prd|(sP3_prd|((~aReductOfIn0(xc,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc))))&(sP1_prd|(~sP3_prd&((aReductOfIn0(xc,xa,xR)|(?[W0]: ((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))|sdtmndtplgtdt0(xa,xR,xc))))),
% 0.12/0.40 inference(NNF_transformation,[status(thm)],[f252])).
% 0.12/0.40 fof(f254,plain,(
% 0.12/0.40 (~sP1_prd|(sP3_prd|((~aReductOfIn0(xc,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc))))&(sP1_prd|(~sP3_prd&((aReductOfIn0(xc,xa,xR)|((aElement0(sK33_skl)&aReductOfIn0(sK33_skl,xa,xR))&sdtmndtplgtdt0(sK33_skl,xR,xc)))|sdtmndtplgtdt0(xa,xR,xc))))),
% 0.12/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl]),skolemize(W0,sK33_skl)],[f253])).
% 0.12/0.40 fof(f257,plain,(
% 0.12/0.40 ~sP1_prd|sP3_prd|~sdtmndtplgtdt0(xa,xR,xc)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f254])).
% 0.12/0.40 fof(f262,plain,(
% 0.12/0.40 ![W0]: ((~sP2_prd(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0)))&(sP2_prd(W0)|((((xb=W0|aReductOfIn0(W0,xb,xR))|(?[W1]: ((aElement0(W1)&aReductOfIn0(W1,xb,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0))))),
% 0.12/0.40 inference(NNF_transformation,[status(thm)],[f179])).
% 0.12/0.40 fof(f263,plain,(
% 0.12/0.40 (![W0]: (~sP2_prd(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0))))&(![W0]: (sP2_prd(W0)|((((xb=W0|aReductOfIn0(W0,xb,xR))|(?[W1]: ((aElement0(W1)&aReductOfIn0(W1,xb,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0))))),
% 0.12/0.41 inference(miniscoping,[status(thm)],[f262])).
% 0.12/0.41 fof(f264,plain,(
% 0.12/0.41 (![W0]: (~sP2_prd(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0))))&(![W0]: (sP2_prd(W0)|((((xb=W0|aReductOfIn0(W0,xb,xR))|((aElement0(sK34_skl(W0))&aReductOfIn0(sK34_skl(W0),xb,xR))&sdtmndtplgtdt0(sK34_skl(W0),xR,W0)))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0))))),
% 0.12/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W1,sK34_skl(W0))],[f263])).
% 0.12/0.41 fof(f265,plain,(
% 0.12/0.41 ![X0]: (~sP2_prd(X0)|~xb=X0)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f264])).
% 0.12/0.41 fof(f268,plain,(
% 0.12/0.41 ![X0]: (~sP2_prd(X0)|~sdtmndtplgtdt0(xb,xR,X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f264])).
% 0.12/0.41 fof(f269,plain,(
% 0.12/0.41 ![X0]: (~sP2_prd(X0)|~sdtmndtasgtdt0(xb,xR,X0))),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f264])).
% 0.12/0.41 fof(f273,plain,(
% 0.12/0.41 (~sP3_prd|((~aReductOfIn0(xb,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb)))&(sP3_prd|((aReductOfIn0(xb,xa,xR)|(?[W0]: ((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))|sdtmndtplgtdt0(xa,xR,xb)))),
% 0.12/0.41 inference(NNF_transformation,[status(thm)],[f251])).
% 0.12/0.41 fof(f274,plain,(
% 0.12/0.41 (~sP3_prd|((~aReductOfIn0(xb,xa,xR)&(![W0]: ((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb)))&(sP3_prd|((aReductOfIn0(xb,xa,xR)|((aElement0(sK35_skl)&aReductOfIn0(sK35_skl,xa,xR))&sdtmndtplgtdt0(sK35_skl,xR,xb)))|sdtmndtplgtdt0(xa,xR,xb)))),
% 0.12/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl]),skolemize(W0,sK35_skl)],[f273])).
% 0.12/0.41 fof(f277,plain,(
% 0.12/0.41 ~sP3_prd|~sdtmndtplgtdt0(xa,xR,xb)),
% 0.12/0.41 inference(cnf_transformation,[status(thm)],[f274])).
% 0.12/0.41 fof(f305,plain,(
% 0.12/0.41 ~aElement0(xc)|sP2_prd(xc)),
% 0.12/0.41 inference(destructive_equality_resolution,[status(thm)],[f235])).
% 0.12/0.41 fof(f307,plain,(
% 0.12/0.41 ~sP2_prd(xb)),
% 0.12/0.41 inference(destructive_equality_resolution,[status(thm)],[f265])).
% 0.12/0.41 fof(f308,plain,(
% 0.12/0.41 sP2_prd(xc)),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f305,f117])).
% 0.12/0.41 fof(f315,plain,(
% 0.12/0.41 ~sP2_prd(sK26_skl)|sP1_prd),
% 0.12/0.41 inference(resolution,[status(thm)],[f269,f219])).
% 0.12/0.41 fof(f318,plain,(
% 0.12/0.41 xa=xb|~sP3_prd),
% 0.12/0.41 inference(resolution,[status(thm)],[f228,f277])).
% 0.12/0.41 fof(f329,plain,(
% 0.12/0.41 ~sP1_prd|sP3_prd|xa=xc),
% 0.12/0.41 inference(resolution,[status(thm)],[f257,f233])).
% 0.12/0.41 fof(f402,plain,(
% 0.12/0.41 ~aElement0(sK26_skl)|sP2_prd(sK26_skl)|sP1_prd),
% 0.12/0.41 inference(resolution,[status(thm)],[f239,f224])).
% 0.12/0.41 fof(f403,plain,(
% 0.12/0.41 sP2_prd(sK26_skl)|sP1_prd),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f402,f207])).
% 0.12/0.41 fof(f406,plain,(
% 0.12/0.41 sP3_prd|xa=xc),
% 0.12/0.41 inference(backward_subsumption_resolution,[status(thm)],[f329,f407])).
% 0.12/0.41 fof(f407,plain,(
% 0.12/0.41 sP1_prd),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f403,f315])).
% 0.12/0.41 fof(f408,plain,(
% 0.12/0.41 xa=xc|xa=xb),
% 0.12/0.41 inference(resolution,[status(thm)],[f406,f318])).
% 0.12/0.41 fof(f413,plain,(
% 0.12/0.41 xa=xc|sdtmndtplgtdt0(xb,xR,xc)|xa=xc),
% 0.12/0.41 inference(paramodulation,[status(thm)],[f408,f233])).
% 0.12/0.41 fof(f421,plain,(
% 0.12/0.41 xa=xc|sdtmndtplgtdt0(xb,xR,xc)),
% 0.12/0.41 inference(duplicate_literals_removal,[status(thm)],[f413])).
% 0.12/0.41 fof(f456,plain,(
% 0.12/0.41 xa=xc|~sP2_prd(xc)),
% 0.12/0.41 inference(resolution,[status(thm)],[f421,f268])).
% 0.12/0.41 fof(f463,plain,(
% 0.12/0.41 xa=xc),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f456,f308])).
% 0.12/0.41 fof(f489,plain,(
% 0.12/0.41 sdtmndtasgtdt0(xc,xR,xb)),
% 0.12/0.41 inference(backward_demodulation,[status(thm)],[f463,f229])).
% 0.12/0.41 fof(f494,plain,(
% 0.12/0.41 ~aElement0(xb)|sP2_prd(xb)),
% 0.12/0.41 inference(resolution,[status(thm)],[f489,f239])).
% 0.12/0.41 fof(f497,plain,(
% 0.12/0.41 sP2_prd(xb)),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f494,f116])).
% 0.12/0.41 fof(f499,plain,(
% 0.12/0.41 $false),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f497,f307])).
% 0.12/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.43 % Elapsed time: 0.067819 seconds
% 0.12/0.43 % CPU time: 0.249408 seconds
% 0.12/0.43 % Total memory used: 80.001 MB
% 0.12/0.43 % Net memory used: 79.581 MB
%------------------------------------------------------------------------------