%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM535+2 : 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 : n012.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:43:08 PM UTC 2026
% Result : Theorem 0.08s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM535+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n012.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 02:38:06 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.42 % Refutation found
% 0.08/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.42 fof(f3,axiom,(
% 0.08/0.42 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f5,definition,(
% 0.08/0.42 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f6,axiom,(
% 0.08/0.42 isFinite0(slcrc0) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f8,axiom,(
% 0.08/0.42 (! [W0] :( ( aSet0(W0)& isCountable0(W0) )=> ~ isFinite0(W0) ) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f10,definition,(
% 0.08/0.42 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f12,axiom,(
% 0.08/0.42 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f13,axiom,(
% 0.08/0.42 (! [W0,W1] :( ( aSet0(W0)& aSet0(W1) )=> ( ( aSubsetOf0(W0,W1)& aSubsetOf0(W1,W0) )=> W0 = W1 ) ) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f14,axiom,(
% 0.08/0.42 (! [W0,W1,W2] :( ( aSet0(W0)& aSet0(W1)& aSet0(W2) )=> ( ( aSubsetOf0(W0,W1)& aSubsetOf0(W1,W2) )=> aSubsetOf0(W0,W2) ) ) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f15,definition,(
% 0.08/0.42 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtpldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& ( aElementOf0(W3,W0)| W3 = W1 ) ) ) )) ) )) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f16,definition,(
% 0.08/0.42 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f17,hypothesis,(
% 0.08/0.42 aSet0(xS) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f18,hypothesis,(
% 0.08/0.42 aElementOf0(xx,xS) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f19,conjecture,(
% 0.08/0.42 ( ( ( aSet0(sdtmndt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(xS,xx))<=> ( aElement0(W0)& aElementOf0(W0,xS)& W0 != xx ) ) ))=> ( ( aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=> ( aElement0(W0)& ( aElementOf0(W0,sdtmndt0(xS,xx))| W0 = xx ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx)) ))| aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) ) ) )& ( ( aSet0(sdtmndt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(xS,xx))<=> ( aElement0(W0)& aElementOf0(W0,xS)& W0 != xx ) ) ))=> ( ( aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=> ( aElement0(W0)& ( aElementOf0(W0,sdtmndt0(xS,xx))| W0 = xx ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS) ) ) ) ) ),
% 0.08/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.42 fof(f20,negated_conjecture,(
% 0.08/0.42 ~(( ( ( aSet0(sdtmndt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(xS,xx))<=> ( aElement0(W0)& aElementOf0(W0,xS)& W0 != xx ) ) ))=> ( ( aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=> ( aElement0(W0)& ( aElementOf0(W0,sdtmndt0(xS,xx))| W0 = xx ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx)) ))| aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)) ) ) )& ( ( aSet0(sdtmndt0(xS,xx))& (! [W0] :( aElementOf0(W0,sdtmndt0(xS,xx))<=> ( aElement0(W0)& aElementOf0(W0,xS)& W0 != xx ) ) ))=> ( ( aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))& (! [W0] :( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=> ( aElement0(W0)& ( aElementOf0(W0,sdtmndt0(xS,xx))| W0 = xx ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS) ) ) ) ) )),
% 0.08/0.42 inference(negated_conjecture,[status(cth)],[f19])).
% 0.08/0.42 fof(f27,plain,(
% 0.08/0.42 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.08/0.42 fof(f28,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f27])).
% 0.08/0.42 fof(f31,plain,(
% 0.08/0.42 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.08/0.42 fof(f32,plain,(
% 0.08/0.42 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f31])).
% 0.08/0.42 fof(f33,plain,(
% 0.08/0.42 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f32])).
% 0.08/0.42 fof(f34,plain,(
% 0.08/0.42 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.08/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f33])).
% 0.08/0.42 fof(f35,plain,(
% 0.08/0.42 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f34])).
% 0.08/0.42 fof(f36,plain,(
% 0.08/0.42 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f34])).
% 0.08/0.42 fof(f37,plain,(
% 0.08/0.42 ![X0]: (X0=slcrc0|~aSet0(X0)|aElementOf0(sK0_skl(X0),X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f34])).
% 0.08/0.42 fof(f38,plain,(
% 0.08/0.42 isFinite0(slcrc0)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.08/0.42 fof(f41,plain,(
% 0.08/0.42 ![W0]: ((~aSet0(W0)|~isCountable0(W0))|~isFinite0(W0))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.08/0.42 fof(f42,plain,(
% 0.08/0.42 ![X0]: (~aSet0(X0)|~isCountable0(X0)|~isFinite0(X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f41])).
% 0.08/0.42 fof(f45,plain,(
% 0.08/0.42 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.08/0.42 fof(f46,plain,(
% 0.08/0.42 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f45])).
% 0.08/0.42 fof(f47,plain,(
% 0.08/0.42 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f46])).
% 0.08/0.42 fof(f48,plain,(
% 0.08/0.42 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK1_skl(W1,W0),W1)&~aElementOf0(sK1_skl(W1,W0),W0)))))))),
% 0.08/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f47])).
% 0.08/0.42 fof(f49,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f48])).
% 0.08/0.42 fof(f50,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f48])).
% 0.08/0.42 fof(f55,plain,(
% 0.08/0.42 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.08/0.42 fof(f56,plain,(
% 0.08/0.42 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f55])).
% 0.08/0.42 fof(f57,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aSet0(W1))|((~aSubsetOf0(W0,W1)|~aSubsetOf0(W1,W0))|W0=W1))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.08/0.42 fof(f58,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aSet0(X1)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,X0)|X0=X1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f57])).
% 0.08/0.42 fof(f59,plain,(
% 0.08/0.42 ![W0,W1,W2]: (((~aSet0(W0)|~aSet0(W1))|~aSet0(W2))|((~aSubsetOf0(W0,W1)|~aSubsetOf0(W1,W2))|aSubsetOf0(W0,W2)))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.08/0.42 fof(f60,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSet0(X2)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,X2)|aSubsetOf0(X0,X2))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f59])).
% 0.08/0.42 fof(f61,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtpldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.08/0.42 fof(f62,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtpldt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1)))&(aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))))))&(W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f61])).
% 0.08/0.42 fof(f63,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f62])).
% 0.08/0.42 fof(f64,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK2_skl(W2,W1,W0),W2)|(~aElement0(sK2_skl(W2,W1,W0))|(~aElementOf0(sK2_skl(W2,W1,W0),W0)&~sK2_skl(W2,W1,W0)=W1)))&(aElementOf0(sK2_skl(W2,W1,W0),W2)|(aElement0(sK2_skl(W2,W1,W0))&(aElementOf0(sK2_skl(W2,W1,W0),W0)|sK2_skl(W2,W1,W0)=W1)))))))))),
% 0.08/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f63])).
% 0.08/0.42 fof(f65,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aSet0(X2))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f64])).
% 0.08/0.42 fof(f66,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|~aElementOf0(X3,X2)|aElement0(X3))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f64])).
% 0.08/0.42 fof(f67,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|~aElementOf0(X3,X2)|aElementOf0(X3,X0)|X3=X1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f64])).
% 0.08/0.42 fof(f68,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aElementOf0(X3,X2)|~aElement0(X3)|~aElementOf0(X3,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f64])).
% 0.08/0.42 fof(f69,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aElementOf0(X3,X2)|~aElement0(X3)|~X3=X1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f64])).
% 0.08/0.42 fof(f74,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.08/0.42 fof(f75,definition,(
% 0.08/0.42 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.08/0.42 fof(f76,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>sP0_prd(W3,W1,W0)))))))),
% 0.08/0.42 inference(formula_renaming,[status(thm)],[f74,f75])).
% 0.08/0.42 fof(f77,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtmndt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))))))&(W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f76])).
% 0.08/0.42 fof(f78,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f77])).
% 0.08/0.42 fof(f79,plain,(
% 0.08/0.42 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK3_skl(W2,W1,W0),W2)|~sP0_prd(sK3_skl(W2,W1,W0),W1,W0))&(aElementOf0(sK3_skl(W2,W1,W0),W2)|sP0_prd(sK3_skl(W2,W1,W0),W1,W0))))))))),
% 0.08/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f78])).
% 0.08/0.42 fof(f80,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|aSet0(X2))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f79])).
% 0.08/0.42 fof(f81,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|~aElementOf0(X3,X2)|sP0_prd(X3,X1,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f79])).
% 0.08/0.42 fof(f82,plain,(
% 0.08/0.42 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|aElementOf0(X3,X2)|~sP0_prd(X3,X1,X0))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f79])).
% 0.08/0.42 fof(f85,plain,(
% 0.08/0.42 aSet0(xS)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.08/0.42 fof(f86,plain,(
% 0.08/0.42 aElementOf0(xx,xS)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f18])).
% 0.08/0.42 fof(f87,plain,(
% 0.08/0.42 (((aSet0(sdtmndt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))<=>((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=>(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx)))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)))))|((aSet0(sdtmndt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))<=>((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=>(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx)))))&((?[W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)))))),
% 0.08/0.42 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.08/0.42 fof(f88,definition,(
% 0.08/0.42 sP1_prd<=>((aSet0(sdtmndt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))<=>((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=>(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx)))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)))))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.08/0.42 fof(f89,plain,(
% 0.08/0.42 sP1_prd|((aSet0(sdtmndt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))<=>((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=>(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx)))))&((?[W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS))))),
% 0.08/0.42 inference(formula_renaming,[status(thm)],[f87,f88])).
% 0.08/0.42 fof(f90,plain,(
% 0.08/0.42 sP1_prd|((aSet0(sdtmndt0(xS,xx))&(![W0]: ((~aElementOf0(W0,sdtmndt0(xS,xx))|((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx))&(aElementOf0(W0,sdtmndt0(xS,xx))|((~aElement0(W0)|~aElementOf0(W0,xS))|W0=xx)))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&(![W0]: ((~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx)))&(aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS))))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f89])).
% 0.08/0.42 fof(f91,plain,(
% 0.08/0.42 sP1_prd|((aSet0(sdtmndt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(xS,xx))|((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx)))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))|((~aElement0(W0)|~aElementOf0(W0,xS))|W0=xx)))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS))))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f90])).
% 0.08/0.42 fof(f92,plain,(
% 0.08/0.42 sP1_prd|((aSet0(sdtmndt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(xS,xx))|((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx)))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))|((~aElement0(W0)|~aElementOf0(W0,xS))|W0=xx)))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx))))))&((aElementOf0(sK4_skl,sdtpldt0(sdtmndt0(xS,xx),xx))&~aElementOf0(sK4_skl,xS))&~aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS))))),
% 0.08/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(W0,sK4_skl)],[f91])).
% 0.08/0.42 fof(f93,plain,(
% 0.08/0.42 sP1_prd|aSet0(sdtmndt0(xS,xx))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.08/0.42 fof(f95,plain,(
% 0.08/0.42 ![X0]: (sP1_prd|~aElementOf0(X0,sdtmndt0(xS,xx))|aElementOf0(X0,xS))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.08/0.42 fof(f101,plain,(
% 0.08/0.42 ![X0]: (sP1_prd|aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(X0)|~aElementOf0(X0,sdtmndt0(xS,xx)))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.08/0.42 fof(f102,plain,(
% 0.08/0.42 ![X0]: (sP1_prd|aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(X0)|~X0=xx)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.08/0.42 fof(f103,plain,(
% 0.08/0.42 sP1_prd|aElementOf0(sK4_skl,sdtpldt0(sdtmndt0(xS,xx),xx))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.08/0.42 fof(f104,plain,(
% 0.08/0.42 sP1_prd|~aElementOf0(sK4_skl,xS)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f92])).
% 0.08/0.42 fof(f106,plain,(
% 0.08/0.42 ![W0,W1,W3]: ((~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))&(sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f75])).
% 0.08/0.42 fof(f107,plain,(
% 0.08/0.42 (![W0,W1,W3]: (~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))&(![W0,W1,W3]: (sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f106])).
% 0.08/0.42 fof(f109,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|aElementOf0(X0,X2))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.08/0.42 fof(f111,plain,(
% 0.08/0.42 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|~aElement0(X0)|~aElementOf0(X0,X2)|X0=X1)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.08/0.42 fof(f112,definition,(
% 0.08/0.42 ![W0]: (sP2_prd(W0)<=>((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.08/0.42 fof(f113,plain,(
% 0.08/0.42 sP1_prd<=>((aSet0(sdtmndt0(xS,xx))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))<=>sP2_prd(W0))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))<=>(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx)))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx)))))),
% 0.08/0.42 inference(formula_renaming,[status(thm)],[f88,f112])).
% 0.08/0.42 fof(f114,plain,(
% 0.08/0.42 (~sP1_prd|((aSet0(sdtmndt0(xS,xx))&(![W0]: ((~aElementOf0(W0,sdtmndt0(xS,xx))|sP2_prd(W0))&(aElementOf0(W0,sdtmndt0(xS,xx))|~sP2_prd(W0)))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&(![W0]: ((~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx)))&(aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx))))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))))&(sP1_prd|((~aSet0(sdtmndt0(xS,xx))|(?[W0]: ((~aElementOf0(W0,sdtmndt0(xS,xx))|~sP2_prd(W0))&(aElementOf0(W0,sdtmndt0(xS,xx))|sP2_prd(W0)))))|((~aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))|(?[W0]: ((~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx)))&(aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx))))))|((![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))|aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f113])).
% 0.08/0.42 fof(f115,plain,(
% 0.08/0.42 (~sP1_prd|((aSet0(sdtmndt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(xS,xx))|sP2_prd(W0)))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))|~sP2_prd(W0)))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx))))))&((?[W0]: (aElementOf0(W0,xS)&~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))&~aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))))&(sP1_prd|((~aSet0(sdtmndt0(xS,xx))|(?[W0]: ((~aElementOf0(W0,sdtmndt0(xS,xx))|~sP2_prd(W0))&(aElementOf0(W0,sdtmndt0(xS,xx))|sP2_prd(W0)))))|((~aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))|(?[W0]: ((~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx)))&(aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx))))))|((![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))|aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f114])).
% 0.08/0.42 fof(f116,plain,(
% 0.08/0.42 (~sP1_prd|((aSet0(sdtmndt0(xS,xx))&((![W0]: (~aElementOf0(W0,sdtmndt0(xS,xx))|sP2_prd(W0)))&(![W0]: (aElementOf0(W0,sdtmndt0(xS,xx))|~sP2_prd(W0)))))&((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))&((![W0]: (~aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xS,xx))|W0=xx))))&(![W0]: (aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xS,xx))&~W0=xx))))))&((aElementOf0(sK5_skl,xS)&~aElementOf0(sK5_skl,sdtpldt0(sdtmndt0(xS,xx),xx)))&~aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))))&(sP1_prd|((~aSet0(sdtmndt0(xS,xx))|((~aElementOf0(sK6_skl,sdtmndt0(xS,xx))|~sP2_prd(sK6_skl))&(aElementOf0(sK6_skl,sdtmndt0(xS,xx))|sP2_prd(sK6_skl))))|((~aSet0(sdtpldt0(sdtmndt0(xS,xx),xx))|((~aElementOf0(sK7_skl,sdtpldt0(sdtmndt0(xS,xx),xx))|(~aElement0(sK7_skl)|(~aElementOf0(sK7_skl,sdtmndt0(xS,xx))&~sK7_skl=xx)))&(aElementOf0(sK7_skl,sdtpldt0(sdtmndt0(xS,xx),xx))|(aElement0(sK7_skl)&(aElementOf0(sK7_skl,sdtmndt0(xS,xx))|sK7_skl=xx)))))|((![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,sdtpldt0(sdtmndt0(xS,xx),xx))))|aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))))),
% 0.08/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl,sK7_skl]),skolemize(W0,sK5_skl),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f115])).
% 0.08/0.42 fof(f117,plain,(
% 0.08/0.42 ~sP1_prd|aSet0(sdtmndt0(xS,xx))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f116])).
% 0.08/0.42 fof(f124,plain,(
% 0.08/0.42 ![X0]: (~sP1_prd|aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(X0)|~X0=xx)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f116])).
% 0.08/0.42 fof(f125,plain,(
% 0.08/0.42 ~sP1_prd|aElementOf0(sK5_skl,xS)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f116])).
% 0.08/0.42 fof(f126,plain,(
% 0.08/0.42 ~sP1_prd|~aElementOf0(sK5_skl,sdtpldt0(sdtmndt0(xS,xx),xx))),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f116])).
% 0.08/0.42 fof(f136,plain,(
% 0.08/0.42 ![W0]: ((~sP2_prd(W0)|((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx))&(sP2_prd(W0)|((~aElement0(W0)|~aElementOf0(W0,xS))|W0=xx)))),
% 0.08/0.42 inference(NNF_transformation,[status(thm)],[f112])).
% 0.08/0.42 fof(f137,plain,(
% 0.08/0.42 (![W0]: (~sP2_prd(W0)|((aElement0(W0)&aElementOf0(W0,xS))&~W0=xx)))&(![W0]: (sP2_prd(W0)|((~aElement0(W0)|~aElementOf0(W0,xS))|W0=xx)))),
% 0.08/0.42 inference(miniscoping,[status(thm)],[f136])).
% 0.08/0.42 fof(f140,plain,(
% 0.08/0.42 ![X0]: (~sP2_prd(X0)|~X0=xx)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f137])).
% 0.08/0.42 fof(f141,plain,(
% 0.08/0.42 ![X0]: (sP2_prd(X0)|~aElement0(X0)|~aElementOf0(X0,xS)|X0=xx)),
% 0.08/0.42 inference(cnf_transformation,[status(thm)],[f137])).
% 0.08/0.42 fof(f142,definition,(
% 0.08/0.42 sQ0_spl <=> (sP1_prd)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f145,definition,(
% 0.08/0.42 sQ1_spl <=> (aSet0(sdtmndt0(xS,xx)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f146,plain,(
% 0.08/0.42 aSet0(sdtmndt0(xS,xx))|~sQ1_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f145])).
% 0.08/0.42 fof(f148,plain,(
% 0.08/0.42 sQ0_spl|sQ1_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f93,f142,f145])).
% 0.08/0.42 fof(f153,definition,(
% 0.08/0.42 ![X0]: (sQ3_spl <=> (~aElementOf0(X0,sdtmndt0(xS,xx))|aElementOf0(X0,xS)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f154,plain,(
% 0.08/0.42 ![X0]: (~aElementOf0(X0,sdtmndt0(xS,xx))|aElementOf0(X0,xS)|~sQ3_spl)),
% 0.08/0.42 inference(component_clause,[status(thm)],[f153])).
% 0.08/0.42 fof(f156,plain,(
% 0.08/0.42 sQ0_spl|sQ3_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f95,f142,f153])).
% 0.08/0.42 fof(f177,definition,(
% 0.08/0.42 ![X0]: (sQ9_spl <=> (aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(X0)|~aElementOf0(X0,sdtmndt0(xS,xx))))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f178,plain,(
% 0.08/0.42 ![X0]: (aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(X0)|~aElementOf0(X0,sdtmndt0(xS,xx))|~sQ9_spl)),
% 0.08/0.42 inference(component_clause,[status(thm)],[f177])).
% 0.08/0.42 fof(f180,plain,(
% 0.08/0.42 sQ0_spl|sQ9_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f101,f142,f177])).
% 0.08/0.42 fof(f181,definition,(
% 0.08/0.42 ![X0]: (sQ10_spl <=> (aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(X0)|~X0=xx))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f182,plain,(
% 0.08/0.42 ![X0]: (aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(X0)|~X0=xx|~sQ10_spl)),
% 0.08/0.42 inference(component_clause,[status(thm)],[f181])).
% 0.08/0.42 fof(f184,plain,(
% 0.08/0.42 sQ0_spl|sQ10_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f102,f142,f181])).
% 0.08/0.42 fof(f185,definition,(
% 0.08/0.42 sQ11_spl <=> (aElementOf0(sK4_skl,sdtpldt0(sdtmndt0(xS,xx),xx)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f186,plain,(
% 0.08/0.42 aElementOf0(sK4_skl,sdtpldt0(sdtmndt0(xS,xx),xx))|~sQ11_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f185])).
% 0.08/0.42 fof(f188,plain,(
% 0.08/0.42 sQ0_spl|sQ11_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f103,f142,f185])).
% 0.08/0.42 fof(f189,definition,(
% 0.08/0.42 sQ12_spl <=> (aElementOf0(sK4_skl,xS))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f191,plain,(
% 0.08/0.42 ~aElementOf0(sK4_skl,xS)|sQ12_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f189])).
% 0.08/0.42 fof(f192,plain,(
% 0.08/0.42 sQ0_spl|~sQ12_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f104,f142,f189])).
% 0.08/0.42 fof(f197,plain,(
% 0.08/0.42 ~sQ0_spl|sQ1_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f117,f142,f145])).
% 0.08/0.42 fof(f210,plain,(
% 0.08/0.42 ~sQ0_spl|sQ10_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f124,f142,f181])).
% 0.08/0.42 fof(f211,definition,(
% 0.08/0.42 sQ16_spl <=> (aElementOf0(sK5_skl,xS))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f212,plain,(
% 0.08/0.42 aElementOf0(sK5_skl,xS)|~sQ16_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f211])).
% 0.08/0.42 fof(f214,plain,(
% 0.08/0.42 ~sQ0_spl|sQ16_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f125,f142,f211])).
% 0.08/0.42 fof(f215,definition,(
% 0.08/0.42 sQ17_spl <=> (aElementOf0(sK5_skl,sdtpldt0(sdtmndt0(xS,xx),xx)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f217,plain,(
% 0.08/0.42 ~aElementOf0(sK5_skl,sdtpldt0(sdtmndt0(xS,xx),xx))|sQ17_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f215])).
% 0.08/0.42 fof(f218,plain,(
% 0.08/0.42 ~sQ0_spl|~sQ17_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f126,f142,f215])).
% 0.08/0.42 fof(f252,plain,(
% 0.08/0.42 aSet0(slcrc0)),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f35])).
% 0.08/0.42 fof(f253,plain,(
% 0.08/0.42 ![X0]: (~aElementOf0(X0,slcrc0))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f36])).
% 0.08/0.42 fof(f256,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aSubsetOf0(X0,X1)|X1=X0)),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f58,f49])).
% 0.08/0.42 fof(f257,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSubsetOf0(X2,X0)|~aSubsetOf0(X0,X1)|aSubsetOf0(X2,X1))),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f60,f49])).
% 0.08/0.42 fof(f258,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtpldt0(X0,X1)))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f65])).
% 0.08/0.42 fof(f259,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~aElementOf0(X2,sdtpldt0(X0,X1))|aElement0(X2))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f66])).
% 0.08/0.42 fof(f260,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~aElementOf0(X2,sdtpldt0(X0,X1))|aElementOf0(X2,X0)|X2=X1)),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f67])).
% 0.08/0.42 fof(f261,plain,(
% 0.08/0.42 ![X0,X1,X3]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X3,sdtpldt0(X0,X1))|~aElement0(X3)|~aElementOf0(X3,X0))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f68])).
% 0.08/0.42 fof(f262,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X2,sdtpldt0(X0,X1))|~aElementOf0(X2,X0))),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f261,f28])).
% 0.08/0.42 fof(f263,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X1,sdtpldt0(X0,X1))|~aElement0(X1))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f69])).
% 0.08/0.42 fof(f264,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X1,sdtpldt0(X0,X1)))),
% 0.08/0.42 inference(duplicate_literals_removal,[status(thm)],[f263])).
% 0.08/0.42 fof(f268,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtmndt0(X0,X1)))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f80])).
% 0.08/0.42 fof(f269,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~aElementOf0(X2,sdtmndt0(X0,X1))|sP0_prd(X2,X1,X0))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f81])).
% 0.08/0.42 fof(f270,plain,(
% 0.08/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|aElementOf0(X2,sdtmndt0(X0,X1))|~sP0_prd(X2,X1,X0))),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f82])).
% 0.08/0.42 fof(f272,plain,(
% 0.08/0.42 ~sP2_prd(xx)),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f140])).
% 0.08/0.42 fof(f273,plain,(
% 0.08/0.42 aElementOf0(xx,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(xx)|~sQ10_spl),
% 0.08/0.42 inference(destructive_equality_resolution,[status(thm)],[f182])).
% 0.08/0.42 fof(f276,plain,(
% 0.08/0.42 sP2_prd(xx)|~aElement0(xx)|xx=xx),
% 0.08/0.42 inference(resolution,[status(thm)],[f86,f141])).
% 0.08/0.42 fof(f277,definition,(
% 0.08/0.42 sQ26_spl <=> (sP2_prd(xx))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f278,plain,(
% 0.08/0.42 sP2_prd(xx)|~sQ26_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f277])).
% 0.08/0.42 fof(f280,definition,(
% 0.08/0.42 sQ27_spl <=> (aElement0(xx))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f281,plain,(
% 0.08/0.42 aElement0(xx)|~sQ27_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f280])).
% 0.08/0.42 fof(f283,definition,(
% 0.08/0.42 sQ28_spl <=> (xx=xx)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f286,plain,(
% 0.08/0.42 sQ26_spl|~sQ27_spl|sQ28_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f276,f277,f280,f283])).
% 0.08/0.42 fof(f288,definition,(
% 0.08/0.42 sQ29_spl <=> (sP2_prd(sK5_skl))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f289,plain,(
% 0.08/0.42 sP2_prd(sK5_skl)|~sQ29_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f288])).
% 0.08/0.42 fof(f291,definition,(
% 0.08/0.42 sQ30_spl <=> (aElement0(sK5_skl))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f292,plain,(
% 0.08/0.42 aElement0(sK5_skl)|~sQ30_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f291])).
% 0.08/0.42 fof(f294,definition,(
% 0.08/0.42 sQ31_spl <=> (sK5_skl=xx)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f295,plain,(
% 0.08/0.42 sK5_skl=xx|~sQ31_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f294])).
% 0.08/0.42 fof(f299,plain,(
% 0.08/0.42 ~aElementOf0(xx,sdtpldt0(sdtmndt0(xS,xx),xx))|~sQ31_spl|sQ17_spl),
% 0.08/0.42 inference(backward_demodulation,[status(thm)],[f295,f217])).
% 0.08/0.42 fof(f301,plain,(
% 0.08/0.42 sP2_prd(xx)|~sQ31_spl|~sQ29_spl),
% 0.08/0.42 inference(forward_demodulation,[status(thm)],[f295,f289])).
% 0.08/0.42 fof(f302,plain,(
% 0.08/0.42 $false|~sQ31_spl|~sQ29_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f301,f272])).
% 0.08/0.42 fof(f303,plain,(
% 0.08/0.42 ~sQ31_spl|~sQ29_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f302])).
% 0.08/0.42 fof(f304,definition,(
% 0.08/0.42 sQ32_spl <=> (aElementOf0(xx,sdtpldt0(sdtmndt0(xS,xx),xx)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f305,plain,(
% 0.08/0.42 aElementOf0(xx,sdtpldt0(sdtmndt0(xS,xx),xx))|~sQ32_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f304])).
% 0.08/0.42 fof(f307,plain,(
% 0.08/0.42 sQ32_spl|~sQ27_spl|~sQ10_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f273,f304,f280,f181])).
% 0.08/0.42 fof(f310,plain,(
% 0.08/0.42 ~aSet0(xS)|aElement0(sK5_skl)|~sQ16_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f28,f212])).
% 0.08/0.42 fof(f311,plain,(
% 0.08/0.42 ~aSet0(xS)|aElement0(xx)),
% 0.08/0.42 inference(resolution,[status(thm)],[f28,f86])).
% 0.08/0.42 fof(f312,definition,(
% 0.08/0.42 sQ33_spl <=> (aSet0(xS))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f314,plain,(
% 0.08/0.42 ~aSet0(xS)|sQ33_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f312])).
% 0.08/0.42 fof(f315,plain,(
% 0.08/0.42 ~sQ33_spl|sQ30_spl|~sQ16_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f310,f312,f291,f211])).
% 0.08/0.42 fof(f316,plain,(
% 0.08/0.42 ~sQ33_spl|sQ27_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f311,f312,f280])).
% 0.08/0.42 fof(f317,plain,(
% 0.08/0.42 $false|sQ33_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f314,f85])).
% 0.08/0.42 fof(f318,plain,(
% 0.08/0.42 sQ33_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f317])).
% 0.08/0.42 fof(f319,plain,(
% 0.08/0.42 $false|~sQ26_spl),
% 0.08/0.42 inference(forward_subsumption_resolution,[status(thm)],[f278,f272])).
% 0.08/0.42 fof(f320,plain,(
% 0.08/0.42 ~sQ26_spl),
% 0.08/0.42 inference(contradiction_clause,[status(thm)],[f319])).
% 0.08/0.42 fof(f321,plain,(
% 0.08/0.42 ![X0]: (~aSet0(X0)|~aSubsetOf0(xS,X0)|aElementOf0(xx,X0))),
% 0.08/0.42 inference(resolution,[status(thm)],[f50,f86])).
% 0.08/0.42 fof(f322,plain,(
% 0.08/0.42 ![X0]: (sP0_prd(xx,X0,xS)|~aElement0(xx)|xx=X0)),
% 0.08/0.42 inference(resolution,[status(thm)],[f111,f86])).
% 0.08/0.42 fof(f323,definition,(
% 0.08/0.42 ![X0]: (sQ34_spl <=> (sP0_prd(xx,X0,xS)|xx=X0))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f326,plain,(
% 0.08/0.42 sQ34_spl|~sQ27_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f322,f323,f280])).
% 0.08/0.42 fof(f333,definition,(
% 0.08/0.42 sQ36_spl <=> (aElement0(sK4_skl))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f334,plain,(
% 0.08/0.42 aElement0(sK4_skl)|~sQ36_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f333])).
% 0.08/0.42 fof(f341,plain,(
% 0.08/0.42 slcrc0=slcrc0|aElementOf0(sK0_skl(slcrc0),slcrc0)),
% 0.08/0.42 inference(resolution,[status(thm)],[f252,f37])).
% 0.08/0.42 fof(f342,plain,(
% 0.08/0.42 ~isCountable0(slcrc0)|~isFinite0(slcrc0)),
% 0.08/0.42 inference(resolution,[status(thm)],[f252,f42])).
% 0.08/0.42 fof(f344,definition,(
% 0.08/0.42 sQ37_spl <=> (slcrc0=slcrc0)),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f347,definition,(
% 0.08/0.42 sQ38_spl <=> (aElementOf0(sK0_skl(slcrc0),slcrc0))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f348,plain,(
% 0.08/0.42 aElementOf0(sK0_skl(slcrc0),slcrc0)|~sQ38_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f347])).
% 0.08/0.42 fof(f350,plain,(
% 0.08/0.42 sQ37_spl|sQ38_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f341,f344,f347])).
% 0.08/0.42 fof(f351,definition,(
% 0.08/0.42 sQ39_spl <=> (isCountable0(slcrc0))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f354,definition,(
% 0.08/0.42 sQ40_spl <=> (isFinite0(slcrc0))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f356,plain,(
% 0.08/0.42 ~isFinite0(slcrc0)|sQ40_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f354])).
% 0.08/0.42 fof(f357,plain,(
% 0.08/0.42 ~sQ39_spl|~sQ40_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f342,f351,f354])).
% 0.08/0.42 fof(f363,plain,(
% 0.08/0.42 ~aSet0(sdtmndt0(xS,xx))|~aElement0(xx)|aElement0(sK4_skl)|~sQ11_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f259,f186])).
% 0.08/0.42 fof(f364,plain,(
% 0.08/0.42 ~sQ1_spl|~sQ27_spl|sQ36_spl|~sQ11_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f363,f145,f280,f333,f185])).
% 0.08/0.42 fof(f365,plain,(
% 0.08/0.42 ![X0,X1]: (~aSet0(X0)|aElementOf0(X1,sdtpldt0(X0,sK4_skl))|~aElementOf0(X1,X0)|~sQ36_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f262,f334])).
% 0.08/0.42 fof(f367,plain,(
% 0.08/0.42 ~aSet0(xS)|aElementOf0(xx,sdtpldt0(xS,sK4_skl))|~sQ36_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f365,f86])).
% 0.08/0.42 fof(f372,definition,(
% 0.08/0.42 sQ43_spl <=> (aElementOf0(xx,sdtpldt0(xS,sK4_skl)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f373,plain,(
% 0.08/0.42 aElementOf0(xx,sdtpldt0(xS,sK4_skl))|~sQ43_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f372])).
% 0.08/0.42 fof(f375,plain,(
% 0.08/0.42 ~sQ33_spl|sQ43_spl|~sQ36_spl),
% 0.08/0.42 inference(split_clause,[status(thm)],[f367,f312,f372,f333])).
% 0.08/0.42 fof(f377,plain,(
% 0.08/0.42 ~aSet0(sdtpldt0(xS,sK4_skl))|aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl))|~sQ43_spl|~sQ36_spl),
% 0.08/0.42 inference(resolution,[status(thm)],[f373,f365])).
% 0.08/0.42 fof(f378,plain,(
% 0.08/0.42 ![X0]: (sP0_prd(xx,X0,sdtpldt0(xS,sK4_skl))|~aElement0(xx)|xx=X0|~sQ43_spl)),
% 0.08/0.42 inference(resolution,[status(thm)],[f373,f111])).
% 0.08/0.42 fof(f382,definition,(
% 0.08/0.42 sQ44_spl <=> (aSet0(sdtpldt0(xS,sK4_skl)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f384,plain,(
% 0.08/0.42 ~aSet0(sdtpldt0(xS,sK4_skl))|sQ44_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f382])).
% 0.08/0.42 fof(f385,definition,(
% 0.08/0.42 sQ45_spl <=> (aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl)))),
% 0.08/0.42 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.08/0.42 fof(f386,plain,(
% 0.08/0.42 aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl))|~sQ45_spl),
% 0.08/0.42 inference(component_clause,[status(thm)],[f385])).
% 0.08/0.42 fof(f388,plain,(
% 0.08/0.42 ~sQ44_spl|sQ45_spl|~sQ43_spl|~sQ36_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f377,f382,f385,f372,f333])).
% 0.08/0.43 fof(f389,definition,(
% 0.08/0.43 ![X0]: (sQ46_spl <=> (sP0_prd(xx,X0,sdtpldt0(xS,sK4_skl))|xx=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f392,plain,(
% 0.08/0.43 sQ46_spl|~sQ27_spl|~sQ43_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f378,f389,f280,f372])).
% 0.08/0.43 fof(f394,plain,(
% 0.08/0.43 ![X0,X1]: (~aSet0(X0)|aElementOf0(X1,sdtpldt0(X0,sK5_skl))|~aElementOf0(X1,X0)|~sQ30_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f292,f262])).
% 0.08/0.43 fof(f396,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK5_skl,X0,xS)|~aElement0(sK5_skl)|sK5_skl=X0|~sQ16_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f212,f111])).
% 0.08/0.43 fof(f397,plain,(
% 0.08/0.43 ![X0]: (~aSet0(X0)|~aSubsetOf0(xS,X0)|aElementOf0(sK5_skl,X0)|~sQ16_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f212,f50])).
% 0.08/0.43 fof(f400,definition,(
% 0.08/0.43 ![X0]: (sQ47_spl <=> (sP0_prd(sK5_skl,X0,xS)|sK5_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f401,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK5_skl,X0,xS)|sK5_skl=X0|~sQ47_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f400])).
% 0.08/0.43 fof(f403,plain,(
% 0.08/0.43 sQ47_spl|~sQ30_spl|~sQ16_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f396,f400,f291,f211])).
% 0.08/0.43 fof(f406,plain,(
% 0.08/0.43 ~aSet0(xS)|aElementOf0(sK5_skl,sdtpldt0(xS,sK5_skl))|~sQ30_spl|~sQ16_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f394,f212])).
% 0.08/0.43 fof(f407,plain,(
% 0.08/0.43 ~aSet0(xS)|aElementOf0(xx,sdtpldt0(xS,sK5_skl))|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f394,f86])).
% 0.08/0.43 fof(f408,definition,(
% 0.08/0.43 sQ48_spl <=> (aElementOf0(sK5_skl,sdtpldt0(xS,sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f409,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtpldt0(xS,sK5_skl))|~sQ48_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f408])).
% 0.08/0.43 fof(f411,plain,(
% 0.08/0.43 ~sQ33_spl|sQ48_spl|~sQ30_spl|~sQ16_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f406,f312,f408,f291,f211])).
% 0.08/0.43 fof(f412,definition,(
% 0.08/0.43 sQ49_spl <=> (aElementOf0(xx,sdtpldt0(xS,sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f413,plain,(
% 0.08/0.43 aElementOf0(xx,sdtpldt0(xS,sK5_skl))|~sQ49_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f412])).
% 0.08/0.43 fof(f415,plain,(
% 0.08/0.43 ~sQ33_spl|sQ49_spl|~sQ30_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f407,f312,f412,f291])).
% 0.08/0.43 fof(f416,plain,(
% 0.08/0.43 ~aSet0(xS)|~aElement0(sK5_skl)|aElementOf0(sK5_skl,xS)|sK5_skl=sK5_skl|~sQ48_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f409,f260])).
% 0.08/0.43 fof(f418,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(xS,sK5_skl))|aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|~sQ48_spl|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f409,f394])).
% 0.08/0.43 fof(f419,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK5_skl,X0,sdtpldt0(xS,sK5_skl))|~aElement0(sK5_skl)|sK5_skl=X0|~sQ48_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f409,f111])).
% 0.08/0.43 fof(f422,definition,(
% 0.08/0.43 sQ50_spl <=> (sK5_skl=sK5_skl)),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f425,plain,(
% 0.08/0.43 ~sQ33_spl|~sQ30_spl|sQ16_spl|sQ50_spl|~sQ48_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f416,f312,f291,f211,f422,f408])).
% 0.08/0.43 fof(f427,definition,(
% 0.08/0.43 sQ51_spl <=> (aSet0(sdtpldt0(xS,sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f429,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(xS,sK5_skl))|sQ51_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f427])).
% 0.08/0.43 fof(f430,definition,(
% 0.08/0.43 sQ52_spl <=> (aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f431,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|~sQ52_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f430])).
% 0.08/0.43 fof(f433,plain,(
% 0.08/0.43 ~sQ51_spl|sQ52_spl|~sQ48_spl|~sQ30_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f418,f427,f430,f408,f291])).
% 0.08/0.43 fof(f434,definition,(
% 0.08/0.43 ![X0]: (sQ53_spl <=> (sP0_prd(sK5_skl,X0,sdtpldt0(xS,sK5_skl))|sK5_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f435,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK5_skl,X0,sdtpldt0(xS,sK5_skl))|sK5_skl=X0|~sQ53_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f434])).
% 0.08/0.43 fof(f437,plain,(
% 0.08/0.43 sQ53_spl|~sQ30_spl|~sQ48_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f419,f434,f291,f408])).
% 0.08/0.43 fof(f441,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(xS,sK5_skl))|aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|~sQ49_spl|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f413,f394])).
% 0.08/0.43 fof(f442,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(xx,X0,sdtpldt0(xS,sK5_skl))|~aElement0(xx)|xx=X0|~sQ49_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f413,f111])).
% 0.08/0.43 fof(f445,definition,(
% 0.08/0.43 sQ54_spl <=> (aElementOf0(xx,xS))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f450,definition,(
% 0.08/0.43 sQ55_spl <=> (aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f451,plain,(
% 0.08/0.43 aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|~sQ55_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f450])).
% 0.08/0.43 fof(f453,plain,(
% 0.08/0.43 ~sQ51_spl|sQ55_spl|~sQ49_spl|~sQ30_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f441,f427,f450,f412,f291])).
% 0.08/0.43 fof(f454,definition,(
% 0.08/0.43 ![X0]: (sQ56_spl <=> (sP0_prd(xx,X0,sdtpldt0(xS,sK5_skl))|xx=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f457,plain,(
% 0.08/0.43 sQ56_spl|~sQ27_spl|~sQ49_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f442,f454,f280,f412])).
% 0.08/0.43 fof(f459,plain,(
% 0.08/0.43 $false|~sQ32_spl|~sQ31_spl|sQ17_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f299,f305])).
% 0.08/0.43 fof(f460,plain,(
% 0.08/0.43 ~sQ32_spl|~sQ31_spl|sQ17_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f459])).
% 0.08/0.43 fof(f463,plain,(
% 0.08/0.43 ![X0]: (~aSet0(sdtpldt0(xS,sK5_skl))|~aElement0(X0)|aElementOf0(sK5_skl,sdtmndt0(sdtpldt0(xS,sK5_skl),X0))|sK5_skl=X0|~sQ53_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f270,f435])).
% 0.08/0.43 fof(f464,plain,(
% 0.08/0.43 ![X0]: (~aSet0(xS)|~aElement0(X0)|aElementOf0(sK5_skl,sdtmndt0(xS,X0))|sK5_skl=X0|~sQ47_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f270,f401])).
% 0.08/0.43 fof(f465,definition,(
% 0.08/0.43 ![X0]: (sQ57_spl <=> (~aElement0(X0)|aElementOf0(sK5_skl,sdtmndt0(sdtpldt0(xS,sK5_skl),X0))|sK5_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f468,plain,(
% 0.08/0.43 ~sQ51_spl|sQ57_spl|~sQ53_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f463,f427,f465,f434])).
% 0.08/0.43 fof(f469,definition,(
% 0.08/0.43 ![X0]: (sQ58_spl <=> (~aElement0(X0)|aElementOf0(sK5_skl,sdtmndt0(xS,X0))|sK5_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f470,plain,(
% 0.08/0.43 ![X0]: (~aElement0(X0)|aElementOf0(sK5_skl,sdtmndt0(xS,X0))|sK5_skl=X0|~sQ58_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f469])).
% 0.08/0.43 fof(f472,plain,(
% 0.08/0.43 ~sQ33_spl|sQ58_spl|~sQ47_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f464,f312,f469,f400])).
% 0.08/0.43 fof(f473,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtmndt0(xS,sK5_skl))|sK5_skl=sK5_skl|~sQ58_spl|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f470,f292])).
% 0.08/0.43 fof(f474,definition,(
% 0.08/0.43 sQ59_spl <=> (aElementOf0(sK5_skl,sdtmndt0(xS,sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f477,plain,(
% 0.08/0.43 sQ59_spl|sQ50_spl|~sQ58_spl|~sQ30_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f473,f474,f422,f469,f291])).
% 0.08/0.43 fof(f479,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtmndt0(xS,xx))|sK5_skl=xx|~sQ27_spl|~sQ58_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f281,f470])).
% 0.08/0.43 fof(f480,plain,(
% 0.08/0.43 ![X0,X1]: (~aSet0(X0)|aElementOf0(X1,sdtpldt0(X0,xx))|~aElementOf0(X1,X0)|~sQ27_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f281,f262])).
% 0.08/0.43 fof(f481,definition,(
% 0.08/0.43 sQ60_spl <=> (aElementOf0(sK5_skl,sdtmndt0(xS,xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f482,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtmndt0(xS,xx))|~sQ60_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f481])).
% 0.08/0.43 fof(f484,plain,(
% 0.08/0.43 sQ60_spl|sQ31_spl|~sQ27_spl|~sQ58_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f479,f481,f294,f280,f469])).
% 0.08/0.43 fof(f505,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtmndt0(xS,sK4_skl))|sK5_skl=sK4_skl|~sQ36_spl|~sQ58_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f334,f470])).
% 0.08/0.43 fof(f507,definition,(
% 0.08/0.43 sQ64_spl <=> (aElementOf0(sK5_skl,sdtmndt0(xS,sK4_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f508,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtmndt0(xS,sK4_skl))|~sQ64_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f507])).
% 0.08/0.43 fof(f510,definition,(
% 0.08/0.43 sQ65_spl <=> (sK5_skl=sK4_skl)),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f511,plain,(
% 0.08/0.43 sK5_skl=sK4_skl|~sQ65_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f510])).
% 0.08/0.43 fof(f512,plain,(
% 0.08/0.43 ~sK5_skl=sK4_skl|sQ65_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f510])).
% 0.08/0.43 fof(f513,plain,(
% 0.08/0.43 sQ64_spl|sQ65_spl|~sQ36_spl|~sQ58_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f505,f507,f510,f333,f469])).
% 0.08/0.43 fof(f516,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(xS,sK4_skl))|aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK4_skl),sK5_skl))|~sQ43_spl|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f373,f394])).
% 0.08/0.43 fof(f520,definition,(
% 0.08/0.43 sQ66_spl <=> (xx=sK4_skl)),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f521,plain,(
% 0.08/0.43 xx=sK4_skl|~sQ66_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f520])).
% 0.08/0.43 fof(f525,definition,(
% 0.08/0.43 sQ67_spl <=> (aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK4_skl),sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f528,plain,(
% 0.08/0.43 ~sQ44_spl|sQ67_spl|~sQ43_spl|~sQ30_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f516,f382,f525,f372,f291])).
% 0.08/0.43 fof(f531,plain,(
% 0.08/0.43 ~aSet0(xS)|~aElement0(sK4_skl)|sP0_prd(sK5_skl,sK4_skl,xS)|~sQ64_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f508,f269])).
% 0.08/0.43 fof(f532,plain,(
% 0.08/0.43 ~aSet0(sdtmndt0(xS,sK4_skl))|aElementOf0(sK5_skl,sdtpldt0(sdtmndt0(xS,sK4_skl),sK5_skl))|~sQ64_spl|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f508,f394])).
% 0.08/0.43 fof(f533,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK5_skl,X0,sdtmndt0(xS,sK4_skl))|~aElement0(sK5_skl)|sK5_skl=X0|~sQ64_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f508,f111])).
% 0.08/0.43 fof(f536,definition,(
% 0.08/0.43 sQ68_spl <=> (sP0_prd(sK5_skl,sK4_skl,xS))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f539,plain,(
% 0.08/0.43 ~sQ33_spl|~sQ36_spl|sQ68_spl|~sQ64_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f531,f312,f333,f536,f507])).
% 0.08/0.43 fof(f540,definition,(
% 0.08/0.43 sQ69_spl <=> (aSet0(sdtmndt0(xS,sK4_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f542,plain,(
% 0.08/0.43 ~aSet0(sdtmndt0(xS,sK4_skl))|sQ69_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f540])).
% 0.08/0.43 fof(f543,definition,(
% 0.08/0.43 sQ70_spl <=> (aElementOf0(sK5_skl,sdtpldt0(sdtmndt0(xS,sK4_skl),sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f546,plain,(
% 0.08/0.43 ~sQ69_spl|sQ70_spl|~sQ64_spl|~sQ30_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f532,f540,f543,f507,f291])).
% 0.08/0.43 fof(f547,definition,(
% 0.08/0.43 ![X0]: (sQ71_spl <=> (sP0_prd(sK5_skl,X0,sdtmndt0(xS,sK4_skl))|sK5_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f550,plain,(
% 0.08/0.43 sQ71_spl|~sQ30_spl|~sQ64_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f533,f547,f291,f507])).
% 0.08/0.43 fof(f592,plain,(
% 0.08/0.43 ![X0]: (~aElement0(X0)|aElementOf0(X0,sdtpldt0(xS,X0)))),
% 0.08/0.43 inference(resolution,[status(thm)],[f85,f264])).
% 0.08/0.43 fof(f593,plain,(
% 0.08/0.43 ![X0]: (~aElement0(X0)|aSet0(sdtmndt0(xS,X0)))),
% 0.08/0.43 inference(resolution,[status(thm)],[f85,f268])).
% 0.08/0.43 fof(f594,plain,(
% 0.08/0.43 ![X0]: (~aElement0(X0)|aSet0(sdtpldt0(xS,X0)))),
% 0.08/0.43 inference(resolution,[status(thm)],[f85,f258])).
% 0.08/0.43 fof(f595,plain,(
% 0.08/0.43 xS=slcrc0|aElementOf0(sK0_skl(xS),xS)),
% 0.08/0.43 inference(resolution,[status(thm)],[f85,f37])).
% 0.08/0.43 fof(f597,plain,(
% 0.08/0.43 aSubsetOf0(xS,xS)),
% 0.08/0.43 inference(resolution,[status(thm)],[f85,f56])).
% 0.08/0.43 fof(f598,definition,(
% 0.08/0.43 sQ73_spl <=> (xS=slcrc0)),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f599,plain,(
% 0.08/0.43 xS=slcrc0|~sQ73_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f598])).
% 0.08/0.43 fof(f601,definition,(
% 0.08/0.43 sQ74_spl <=> (aElementOf0(sK0_skl(xS),xS))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f602,plain,(
% 0.08/0.43 aElementOf0(sK0_skl(xS),xS)|~sQ74_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f601])).
% 0.08/0.43 fof(f604,plain,(
% 0.08/0.43 sQ73_spl|sQ74_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f595,f598,f601])).
% 0.08/0.43 fof(f623,plain,(
% 0.08/0.43 aElementOf0(xx,slcrc0)|~sQ73_spl),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f599,f86])).
% 0.08/0.43 fof(f688,plain,(
% 0.08/0.43 ![X0]: (~aSet0(xS)|~aSet0(X0)|~aSubsetOf0(xS,X0)|aSubsetOf0(xS,X0))),
% 0.08/0.43 inference(resolution,[status(thm)],[f597,f257])).
% 0.08/0.43 fof(f690,plain,(
% 0.08/0.43 ~aSet0(xS)|~aSubsetOf0(xS,xS)|xS=xS),
% 0.08/0.43 inference(resolution,[status(thm)],[f597,f256])).
% 0.08/0.43 fof(f692,definition,(
% 0.08/0.43 ![X0]: (sQ77_spl <=> (~aSet0(X0)|~aSubsetOf0(xS,X0)|aSubsetOf0(xS,X0)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f695,plain,(
% 0.08/0.43 ~sQ33_spl|sQ77_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f688,f312,f692])).
% 0.08/0.43 fof(f697,definition,(
% 0.08/0.43 sQ78_spl <=> (aSubsetOf0(xS,xS))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f699,plain,(
% 0.08/0.43 ~aSubsetOf0(xS,xS)|sQ78_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f697])).
% 0.08/0.43 fof(f700,definition,(
% 0.08/0.43 sQ79_spl <=> (xS=xS)),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f703,plain,(
% 0.08/0.43 ~sQ33_spl|~sQ78_spl|sQ79_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f690,f312,f697,f700])).
% 0.08/0.43 fof(f705,plain,(
% 0.08/0.43 $false|sQ78_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f699,f597])).
% 0.08/0.43 fof(f706,plain,(
% 0.08/0.43 sQ78_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f705])).
% 0.08/0.43 fof(f707,plain,(
% 0.08/0.43 ~aSet0(xS)|aElementOf0(sK0_skl(xS),sdtpldt0(xS,sK5_skl))|~sQ74_spl|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f602,f394])).
% 0.08/0.43 fof(f708,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK0_skl(xS),X0,xS)|~aElement0(sK0_skl(xS))|sK0_skl(xS)=X0|~sQ74_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f602,f111])).
% 0.08/0.43 fof(f710,plain,(
% 0.08/0.43 ~aSet0(xS)|aElement0(sK0_skl(xS))|~sQ74_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f602,f28])).
% 0.08/0.43 fof(f711,definition,(
% 0.08/0.43 sQ80_spl <=> (aElementOf0(sK0_skl(xS),sdtpldt0(xS,sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f712,plain,(
% 0.08/0.43 aElementOf0(sK0_skl(xS),sdtpldt0(xS,sK5_skl))|~sQ80_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f711])).
% 0.08/0.43 fof(f714,plain,(
% 0.08/0.43 ~sQ33_spl|sQ80_spl|~sQ74_spl|~sQ30_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f707,f312,f711,f601,f291])).
% 0.08/0.43 fof(f715,definition,(
% 0.08/0.43 ![X0]: (sQ81_spl <=> (sP0_prd(sK0_skl(xS),X0,xS)|sK0_skl(xS)=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f718,definition,(
% 0.08/0.43 sQ82_spl <=> (aElement0(sK0_skl(xS)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f721,plain,(
% 0.08/0.43 sQ81_spl|~sQ82_spl|~sQ74_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f708,f715,f718,f601])).
% 0.08/0.43 fof(f722,plain,(
% 0.08/0.43 ~sQ33_spl|sQ82_spl|~sQ74_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f710,f312,f718,f601])).
% 0.08/0.43 fof(f776,plain,(
% 0.08/0.43 aSet0(sdtpldt0(xS,sK4_skl))|~sQ36_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f594,f334])).
% 0.08/0.43 fof(f778,plain,(
% 0.08/0.43 aSet0(sdtpldt0(xS,sK5_skl))|~sQ30_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f594,f292])).
% 0.08/0.43 fof(f779,plain,(
% 0.08/0.43 $false|sQ44_spl|~sQ36_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f776,f384])).
% 0.08/0.43 fof(f780,plain,(
% 0.08/0.43 sQ44_spl|~sQ36_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f779])).
% 0.08/0.43 fof(f781,plain,(
% 0.08/0.43 $false|sQ51_spl|~sQ30_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f778,f429])).
% 0.08/0.43 fof(f782,plain,(
% 0.08/0.43 sQ51_spl|~sQ30_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f781])).
% 0.08/0.43 fof(f783,plain,(
% 0.08/0.43 $false|~sQ73_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f623,f253])).
% 0.08/0.43 fof(f784,plain,(
% 0.08/0.43 ~sQ73_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f783])).
% 0.08/0.43 fof(f795,plain,(
% 0.08/0.43 aSet0(sdtmndt0(xS,sK4_skl))|~sQ36_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f593,f334])).
% 0.08/0.43 fof(f797,plain,(
% 0.08/0.43 aElementOf0(sK4_skl,sdtpldt0(xS,sK4_skl))|~sQ36_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f592,f334])).
% 0.08/0.43 fof(f798,plain,(
% 0.08/0.43 aElementOf0(xx,sdtpldt0(xS,xx))|~sQ27_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f592,f281])).
% 0.08/0.43 fof(f801,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK4_skl,X0,sdtpldt0(xS,sK4_skl))|~aElement0(sK4_skl)|sK4_skl=X0|~sQ36_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f797,f111])).
% 0.08/0.43 fof(f809,definition,(
% 0.08/0.43 ![X0]: (sQ84_spl <=> (sP0_prd(sK4_skl,X0,sdtpldt0(xS,sK4_skl))|sK4_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f810,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK4_skl,X0,sdtpldt0(xS,sK4_skl))|sK4_skl=X0|~sQ84_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f809])).
% 0.08/0.43 fof(f812,plain,(
% 0.08/0.43 sQ84_spl|~sQ36_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f801,f809,f333])).
% 0.08/0.43 fof(f816,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(xx,X0,sdtpldt0(xS,xx))|~aElement0(xx)|xx=X0|~sQ27_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f798,f111])).
% 0.08/0.43 fof(f821,definition,(
% 0.08/0.43 ![X0]: (sQ85_spl <=> (sP0_prd(xx,X0,sdtpldt0(xS,xx))|xx=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f824,plain,(
% 0.08/0.43 sQ85_spl|~sQ27_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f816,f821,f280])).
% 0.08/0.43 fof(f829,plain,(
% 0.08/0.43 ~aSet0(xS)|aElementOf0(xx,xS)),
% 0.08/0.43 inference(resolution,[status(thm)],[f321,f597])).
% 0.08/0.43 fof(f830,plain,(
% 0.08/0.43 ~sQ33_spl|sQ54_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f829,f312,f445])).
% 0.08/0.43 fof(f831,plain,(
% 0.08/0.43 sP2_prd(sK0_skl(xS))|~aElement0(sK0_skl(xS))|sK0_skl(xS)=xx|~sQ74_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f141,f602])).
% 0.08/0.43 fof(f833,definition,(
% 0.08/0.43 sQ87_spl <=> (sP2_prd(sK0_skl(xS)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f834,plain,(
% 0.08/0.43 sP2_prd(sK0_skl(xS))|~sQ87_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f833])).
% 0.08/0.43 fof(f836,definition,(
% 0.08/0.43 sQ88_spl <=> (sK0_skl(xS)=xx)),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f837,plain,(
% 0.08/0.43 sK0_skl(xS)=xx|~sQ88_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f836])).
% 0.08/0.43 fof(f839,plain,(
% 0.08/0.43 sQ87_spl|~sQ82_spl|sQ88_spl|~sQ74_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f831,f833,f718,f836,f601])).
% 0.08/0.43 fof(f843,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(xx,X0,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl))|~aElement0(xx)|xx=X0|~sQ45_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f386,f111])).
% 0.08/0.43 fof(f848,definition,(
% 0.08/0.43 ![X0]: (sQ89_spl <=> (sP0_prd(xx,X0,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl))|xx=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f851,plain,(
% 0.08/0.43 sQ89_spl|~sQ27_spl|~sQ45_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f843,f848,f280,f385])).
% 0.08/0.43 fof(f917,plain,(
% 0.08/0.43 ![X0]: (sK4_skl=X0|~aSet0(sdtpldt0(xS,sK4_skl))|~aElement0(X0)|aElementOf0(sK4_skl,sdtmndt0(sdtpldt0(xS,sK4_skl),X0))|~sQ84_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f810,f270])).
% 0.08/0.43 fof(f919,definition,(
% 0.08/0.43 ![X0]: (sQ96_spl <=> (sK4_skl=X0|~aElement0(X0)|aElementOf0(sK4_skl,sdtmndt0(sdtpldt0(xS,sK4_skl),X0))))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f922,plain,(
% 0.08/0.43 sQ96_spl|~sQ44_spl|~sQ84_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f917,f919,f382,f809])).
% 0.08/0.43 fof(f923,plain,(
% 0.08/0.43 ~aSet0(sdtmndt0(xS,xx))|~aElement0(xx)|aElementOf0(sK4_skl,sdtmndt0(xS,xx))|sK4_skl=xx|~sQ11_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f186,f260])).
% 0.08/0.43 fof(f928,definition,(
% 0.08/0.43 sQ97_spl <=> (aElementOf0(sK4_skl,sdtmndt0(xS,xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f929,plain,(
% 0.08/0.43 aElementOf0(sK4_skl,sdtmndt0(xS,xx))|~sQ97_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f928])).
% 0.08/0.43 fof(f931,plain,(
% 0.08/0.43 ~sQ1_spl|~sQ27_spl|sQ97_spl|sQ66_spl|~sQ11_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f923,f145,f280,f928,f520,f185])).
% 0.08/0.43 fof(f939,plain,(
% 0.08/0.43 ~aElementOf0(xx,xS)|~sQ66_spl|sQ12_spl),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f521,f191])).
% 0.08/0.43 fof(f960,plain,(
% 0.08/0.43 $false|~sQ66_spl|sQ12_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f939,f86])).
% 0.08/0.43 fof(f961,plain,(
% 0.08/0.43 ~sQ66_spl|sQ12_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f960])).
% 0.08/0.43 fof(f966,plain,(
% 0.08/0.43 aElementOf0(sK4_skl,xS)|~sQ97_spl|~sQ3_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f929,f154])).
% 0.08/0.43 fof(f972,plain,(
% 0.08/0.43 $false|sQ12_spl|~sQ97_spl|~sQ3_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f966,f191])).
% 0.08/0.43 fof(f973,plain,(
% 0.08/0.43 sQ12_spl|~sQ97_spl|~sQ3_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f972])).
% 0.08/0.43 fof(f974,plain,(
% 0.08/0.43 $false|~sQ36_spl|sQ69_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f542,f795])).
% 0.08/0.43 fof(f975,plain,(
% 0.08/0.43 ~sQ36_spl|sQ69_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f974])).
% 0.08/0.43 fof(f978,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK5_skl,X0,xS)|sK4_skl=X0|~sQ65_spl|~sQ47_spl)),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f511,f401])).
% 0.08/0.43 fof(f981,plain,(
% 0.08/0.43 aElementOf0(sK4_skl,sdtmndt0(xS,xx))|~sQ65_spl|~sQ60_spl),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f511,f482])).
% 0.08/0.43 fof(f984,plain,(
% 0.08/0.43 ![X0]: (~aSet0(X0)|~aSubsetOf0(xS,X0)|aElementOf0(sK4_skl,X0)|~sQ65_spl|~sQ16_spl)),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f511,f397])).
% 0.08/0.43 fof(f997,plain,(
% 0.08/0.43 aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(xS,sK5_skl),sK4_skl))|~sQ65_spl|~sQ52_spl),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f511,f431])).
% 0.08/0.43 fof(f999,plain,(
% 0.08/0.43 aElementOf0(sK0_skl(xS),sdtpldt0(xS,sK4_skl))|~sQ65_spl|~sQ80_spl),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f511,f712])).
% 0.08/0.43 fof(f1006,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK4_skl,X0,xS)|sK4_skl=X0|~sQ65_spl|~sQ47_spl)),
% 0.08/0.43 inference(forward_demodulation,[status(thm)],[f511,f978])).
% 0.08/0.43 fof(f1015,plain,(
% 0.08/0.43 aElementOf0(sK4_skl,sdtpldt0(sdtpldt0(xS,sK5_skl),sK4_skl))|~sQ65_spl|~sQ52_spl),
% 0.08/0.43 inference(forward_demodulation,[status(thm)],[f511,f997])).
% 0.08/0.43 fof(f1016,plain,(
% 0.08/0.43 aElementOf0(sK4_skl,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl))|~sQ65_spl|~sQ52_spl),
% 0.08/0.43 inference(forward_demodulation,[status(thm)],[f511,f1015])).
% 0.08/0.43 fof(f1053,plain,(
% 0.08/0.43 ![X0]: (sK4_skl=X0|~aSet0(xS)|~aElement0(X0)|aElementOf0(sK4_skl,sdtmndt0(xS,X0))|~sQ65_spl|~sQ47_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f1006,f270])).
% 0.08/0.43 fof(f1055,definition,(
% 0.08/0.43 ![X0]: (sQ100_spl <=> (sK4_skl=X0|~aElement0(X0)|aElementOf0(sK4_skl,sdtmndt0(xS,X0))))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1058,plain,(
% 0.08/0.43 sQ100_spl|~sQ33_spl|~sQ65_spl|~sQ47_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1053,f1055,f312,f510,f400])).
% 0.08/0.43 fof(f1074,definition,(
% 0.08/0.43 ![X0]: (sQ103_spl <=> (sK4_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1075,plain,(
% 0.08/0.43 ![X0]: (sK4_skl=X0|~sQ103_spl)),
% 0.08/0.43 inference(component_clause,[status(thm)],[f1074])).
% 0.08/0.43 fof(f1087,plain,(
% 0.08/0.43 sP2_prd(xx)|~sQ88_spl|~sQ87_spl),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f837,f834])).
% 0.08/0.43 fof(f1091,plain,(
% 0.08/0.43 $false|sQ40_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f356,f38])).
% 0.08/0.43 fof(f1092,plain,(
% 0.08/0.43 sQ40_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f1091])).
% 0.08/0.43 fof(f1093,plain,(
% 0.08/0.43 $false|~sQ38_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f348,f253])).
% 0.08/0.43 fof(f1094,plain,(
% 0.08/0.43 ~sQ38_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f1093])).
% 0.08/0.43 fof(f1105,plain,(
% 0.08/0.43 aSubsetOf0(sdtmndt0(xS,xx),sdtmndt0(xS,xx))|~sQ1_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f146,f56])).
% 0.08/0.43 fof(f1197,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK0_skl(xS),X0,sdtpldt0(xS,sK4_skl))|~aElement0(sK0_skl(xS))|sK0_skl(xS)=X0|~sQ65_spl|~sQ80_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f999,f111])).
% 0.08/0.43 fof(f1200,definition,(
% 0.08/0.43 sQ108_spl <=> (sK0_skl(xS)=sK4_skl)),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1201,plain,(
% 0.08/0.43 sK0_skl(xS)=sK4_skl|~sQ108_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f1200])).
% 0.08/0.43 fof(f1205,definition,(
% 0.08/0.43 ![X0]: (sQ109_spl <=> (sP0_prd(sK0_skl(xS),X0,sdtpldt0(xS,sK4_skl))|sK0_skl(xS)=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1208,plain,(
% 0.08/0.43 sQ109_spl|~sQ82_spl|~sQ65_spl|~sQ80_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1197,f1205,f718,f510,f711])).
% 0.08/0.43 fof(f1211,plain,(
% 0.08/0.43 ~aSet0(xS)|aElementOf0(sK4_skl,xS)|~sQ65_spl|~sQ16_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f984,f597])).
% 0.08/0.43 fof(f1212,plain,(
% 0.08/0.43 ~sQ33_spl|sQ12_spl|~sQ65_spl|~sQ16_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1211,f312,f189,f510,f211])).
% 0.08/0.43 fof(f1224,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK4_skl,X0,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl))|~aElement0(sK4_skl)|sK4_skl=X0|~sQ65_spl|~sQ52_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f1016,f111])).
% 0.08/0.43 fof(f1227,definition,(
% 0.08/0.43 sQ110_spl <=> (aElementOf0(sK4_skl,sdtpldt0(xS,sK4_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1232,definition,(
% 0.08/0.43 ![X0]: (sQ111_spl <=> (sP0_prd(sK4_skl,X0,sdtpldt0(sdtpldt0(xS,sK4_skl),sK4_skl))|sK4_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1235,plain,(
% 0.08/0.43 sQ111_spl|~sQ36_spl|~sQ65_spl|~sQ52_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1224,f1232,f333,f510,f430])).
% 0.08/0.43 fof(f1237,plain,(
% 0.08/0.43 ![X0]: (sK4_skl=X0|aElementOf0(sK4_skl,sdtpldt0(xS,sK4_skl))|~sQ84_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f810,f109])).
% 0.08/0.43 fof(f1241,plain,(
% 0.08/0.43 sQ103_spl|sQ110_spl|~sQ84_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1237,f1074,f1227,f809])).
% 0.08/0.43 fof(f1244,plain,(
% 0.08/0.43 ![X0]: (~aSet0(sdtmndt0(xS,xx))|~aSet0(X0)|~aSubsetOf0(sdtmndt0(xS,xx),X0)|aSubsetOf0(sdtmndt0(xS,xx),X0)|~sQ1_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f1105,f257])).
% 0.08/0.43 fof(f1246,plain,(
% 0.08/0.43 ~aSet0(sdtmndt0(xS,xx))|~aSubsetOf0(sdtmndt0(xS,xx),sdtmndt0(xS,xx))|sdtmndt0(xS,xx)=sdtmndt0(xS,xx)|~sQ1_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f1105,f256])).
% 0.08/0.43 fof(f1248,definition,(
% 0.08/0.43 ![X0]: (sQ112_spl <=> (~aSet0(X0)|~aSubsetOf0(sdtmndt0(xS,xx),X0)|aSubsetOf0(sdtmndt0(xS,xx),X0)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1251,plain,(
% 0.08/0.43 ~sQ1_spl|sQ112_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1244,f145,f1248])).
% 0.08/0.43 fof(f1253,definition,(
% 0.08/0.43 sQ113_spl <=> (aSubsetOf0(sdtmndt0(xS,xx),sdtmndt0(xS,xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1255,plain,(
% 0.08/0.43 ~aSubsetOf0(sdtmndt0(xS,xx),sdtmndt0(xS,xx))|sQ113_spl),
% 0.08/0.43 inference(component_clause,[status(thm)],[f1253])).
% 0.08/0.43 fof(f1256,definition,(
% 0.08/0.43 sQ114_spl <=> (sdtmndt0(xS,xx)=sdtmndt0(xS,xx))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1259,plain,(
% 0.08/0.43 ~sQ1_spl|~sQ113_spl|sQ114_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1246,f145,f1253,f1256])).
% 0.08/0.43 fof(f1261,plain,(
% 0.08/0.43 $false|~sQ1_spl|sQ113_spl),
% 0.08/0.43 inference(forward_subsumption_resolution,[status(thm)],[f1255,f1105])).
% 0.08/0.43 fof(f1262,plain,(
% 0.08/0.43 ~sQ1_spl|sQ113_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f1261])).
% 0.08/0.43 fof(f1276,plain,(
% 0.08/0.43 aElementOf0(sK4_skl,sdtpldt0(sdtmndt0(xS,xx),xx))|~aElement0(sK4_skl)|~sQ9_spl|~sQ65_spl|~sQ60_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f178,f981])).
% 0.08/0.43 fof(f1277,plain,(
% 0.08/0.43 sQ11_spl|~sQ36_spl|~sQ9_spl|~sQ65_spl|~sQ60_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1276,f185,f333,f177,f510,f481])).
% 0.08/0.43 fof(f1285,plain,(
% 0.08/0.43 sQ26_spl|~sQ88_spl|~sQ87_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1087,f277,f836,f833])).
% 0.08/0.43 fof(f1287,plain,(
% 0.08/0.43 xx=sK4_skl|~sQ88_spl|~sQ108_spl),
% 0.08/0.43 inference(backward_demodulation,[status(thm)],[f837,f1201])).
% 0.08/0.43 fof(f1289,plain,(
% 0.08/0.43 $false|~sQ103_spl|sQ65_spl),
% 0.08/0.43 inference(backward_subsumption_resolution,[status(thm)],[f512,f1075])).
% 0.08/0.43 fof(f1293,plain,(
% 0.08/0.43 sQ66_spl|~sQ88_spl|~sQ108_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1287,f520,f836,f1200])).
% 0.08/0.43 fof(f1294,plain,(
% 0.08/0.43 ~sQ103_spl|sQ65_spl),
% 0.08/0.43 inference(contradiction_clause,[status(thm)],[f1289])).
% 0.08/0.43 fof(f1367,plain,(
% 0.08/0.43 ![X0]: (sK5_skl=X0|aElementOf0(sK5_skl,xS)|~sQ47_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f401,f109])).
% 0.08/0.43 fof(f1371,definition,(
% 0.08/0.43 ![X0]: (sQ116_spl <=> (sK5_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1374,plain,(
% 0.08/0.43 sQ116_spl|sQ16_spl|~sQ47_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1367,f1371,f211,f400])).
% 0.08/0.43 fof(f1416,plain,(
% 0.08/0.43 ![X0]: (sK5_skl=X0|aElementOf0(sK5_skl,sdtpldt0(xS,sK5_skl))|~sQ53_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f435,f109])).
% 0.08/0.43 fof(f1420,plain,(
% 0.08/0.43 sQ116_spl|sQ48_spl|~sQ53_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1416,f1371,f408,f434])).
% 0.08/0.43 fof(f1423,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(xS,sK5_skl))|~aElement0(sK5_skl)|aElementOf0(sK5_skl,sdtpldt0(xS,sK5_skl))|sK5_skl=sK5_skl|~sQ52_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f431,f260])).
% 0.08/0.43 fof(f1425,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(sK5_skl,X0,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|~aElement0(sK5_skl)|sK5_skl=X0|~sQ52_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f431,f111])).
% 0.08/0.43 fof(f1428,plain,(
% 0.08/0.43 ~sQ51_spl|~sQ30_spl|sQ48_spl|sQ50_spl|~sQ52_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1423,f427,f291,f408,f422,f430])).
% 0.08/0.43 fof(f1430,definition,(
% 0.08/0.43 ![X0]: (sQ117_spl <=> (sP0_prd(sK5_skl,X0,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|sK5_skl=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1433,plain,(
% 0.08/0.43 sQ117_spl|~sQ30_spl|~sQ52_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1425,f1430,f291,f430])).
% 0.08/0.43 fof(f1434,definition,(
% 0.08/0.43 sQ118_spl <=> (aSet0(sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1440,plain,(
% 0.08/0.43 ![X0]: (sP0_prd(xx,X0,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|~aElement0(xx)|xx=X0|~sQ55_spl)),
% 0.08/0.43 inference(resolution,[status(thm)],[f451,f111])).
% 0.08/0.43 fof(f1445,definition,(
% 0.08/0.43 ![X0]: (sQ119_spl <=> (sP0_prd(xx,X0,sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|xx=X0))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1448,plain,(
% 0.08/0.43 sQ119_spl|~sQ27_spl|~sQ55_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1440,f1445,f280,f450])).
% 0.08/0.43 fof(f1450,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl),xx))|~sQ27_spl|~sQ52_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f480,f431])).
% 0.08/0.43 fof(f1451,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(xS,sK5_skl))|aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(xS,sK5_skl),xx))|~sQ27_spl|~sQ48_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f480,f409])).
% 0.08/0.43 fof(f1452,plain,(
% 0.08/0.43 ~aSet0(sdtmndt0(xS,xx))|aElementOf0(sK5_skl,sdtpldt0(sdtmndt0(xS,xx),xx))|~sQ27_spl|~sQ60_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f480,f482])).
% 0.08/0.43 fof(f1453,plain,(
% 0.08/0.43 ~aSet0(xS)|aElementOf0(sK5_skl,sdtpldt0(xS,xx))|~sQ27_spl|~sQ16_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f480,f212])).
% 0.08/0.43 fof(f1454,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl))|aElementOf0(xx,sdtpldt0(sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl),xx))|~sQ27_spl|~sQ55_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f480,f451])).
% 0.08/0.43 fof(f1455,plain,(
% 0.08/0.43 ~aSet0(sdtpldt0(xS,sK5_skl))|aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK5_skl),xx))|~sQ27_spl|~sQ49_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f480,f413])).
% 0.08/0.43 fof(f1457,plain,(
% 0.08/0.43 ~aSet0(xS)|aElementOf0(xx,sdtpldt0(xS,xx))|~sQ27_spl),
% 0.08/0.43 inference(resolution,[status(thm)],[f480,f86])).
% 0.08/0.43 fof(f1458,definition,(
% 0.08/0.43 sQ120_spl <=> (aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl),xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1461,plain,(
% 0.08/0.43 ~sQ118_spl|sQ120_spl|~sQ27_spl|~sQ52_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1450,f1434,f1458,f280,f430])).
% 0.08/0.43 fof(f1462,definition,(
% 0.08/0.43 sQ121_spl <=> (aElementOf0(sK5_skl,sdtpldt0(sdtpldt0(xS,sK5_skl),xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1465,plain,(
% 0.08/0.43 ~sQ51_spl|sQ121_spl|~sQ27_spl|~sQ48_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1451,f427,f1462,f280,f408])).
% 0.08/0.43 fof(f1466,plain,(
% 0.08/0.43 ~sQ1_spl|sQ17_spl|~sQ27_spl|~sQ60_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1452,f145,f215,f280,f481])).
% 0.08/0.43 fof(f1467,definition,(
% 0.08/0.43 sQ122_spl <=> (aElementOf0(sK5_skl,sdtpldt0(xS,xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1470,plain,(
% 0.08/0.43 ~sQ33_spl|sQ122_spl|~sQ27_spl|~sQ16_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1453,f312,f1467,f280,f211])).
% 0.08/0.43 fof(f1471,definition,(
% 0.08/0.43 sQ123_spl <=> (aElementOf0(xx,sdtpldt0(sdtpldt0(sdtpldt0(xS,sK5_skl),sK5_skl),xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1474,plain,(
% 0.08/0.43 ~sQ118_spl|sQ123_spl|~sQ27_spl|~sQ55_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1454,f1434,f1471,f280,f450])).
% 0.08/0.43 fof(f1475,definition,(
% 0.08/0.43 sQ124_spl <=> (aElementOf0(xx,sdtpldt0(sdtpldt0(xS,sK5_skl),xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1478,plain,(
% 0.08/0.43 ~sQ51_spl|sQ124_spl|~sQ27_spl|~sQ49_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1455,f427,f1475,f280,f412])).
% 0.08/0.43 fof(f1483,definition,(
% 0.08/0.43 sQ126_spl <=> (aElementOf0(xx,sdtpldt0(xS,xx)))),
% 0.08/0.43 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.08/0.43 fof(f1486,plain,(
% 0.08/0.43 ~sQ33_spl|sQ126_spl|~sQ27_spl),
% 0.08/0.43 inference(split_clause,[status(thm)],[f1457,f312,f1483,f280])).
% 0.08/0.43 fof(f1487,plain,(
% 0.08/0.43 $false),
% 0.08/0.43 inference(sat_refutation,[status(thm)],[f148,f156,f180,f184,f188,f192,f197,f210,f214,f218,f286,f303,f307,f315,f316,f318,f320,f326,f350,f357,f364,f375,f388,f392,f403,f411,f415,f425,f433,f437,f453,f457,f460,f468,f472,f477,f484,f513,f528,f539,f546,f550,f604,f695,f703,f706,f714,f721,f722,f780,f782,f784,f812,f824,f830,f839,f851,f922,f931,f961,f973,f975,f1058,f1092,f1094,f1208,f1212,f1235,f1241,f1251,f1259,f1262,f1277,f1285,f1293,f1294,f1374,f1420,f1428,f1433,f1448,f1461,f1465,f1466,f1470,f1474,f1478,f1486])).
% 0.08/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.47 % Elapsed time: 0.091609 seconds
% 0.08/0.47 % CPU time: 0.335858 seconds
% 0.08/0.47 % Total memory used: 83.550 MB
% 0.08/0.47 % Net memory used: 83.134 MB
%------------------------------------------------------------------------------