%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV469+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 02:50:54 PM UTC 2026
% Result : Theorem 7.36s 1.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV469+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 08:53:19 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 7.36/1.47 % Refutation found
% 7.36/1.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.36/1.47 % SZS output start CNFRefutation for theBenchmark
% 7.36/1.47 fof(f3,axiom,(
% 7.36/1.47 (! [P] : leq(s(zero),host(P)) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f5,axiom,(
% 7.36/1.47 (! [P] : leq(host(P),nbr_proc) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f36,axiom,(
% 7.36/1.47 (! [X,Q] : head(cons(X,Q)) = X )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f42,axiom,(
% 7.36/1.47 (! [X,Q] : q_nil != cons(X,Q) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f44,axiom,(
% 7.36/1.47 (! [X] : cons(X,q_nil) = snoc(q_nil,X) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f47,axiom,(
% 7.36/1.47 (! [X,Y,Q] :( elem(X,cons(Y,Q))<=> ( X = Y| elem(X,Q) ) ) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f49,axiom,(
% 7.36/1.47 (! [X] :( pidElem(X)<=> (? [Y] :( X = m_Halt(Y)| X = m_Down(Y) ) )) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f60,axiom,(
% 7.36/1.47 (! [X] : leq(X,X) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f61,axiom,(
% 7.36/1.47 (! [X,Y] :( leq(X,Y)| leq(Y,X) ) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f62,axiom,(
% 7.36/1.47 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f65,axiom,(
% 7.36/1.47 (! [X,Y] :( leq(X,s(Y))<=> ( X = s(Y)| leq(X,Y) ) ) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f67,conjecture,(
% 7.36/1.47 (! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid0),queue(host(Z))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& setIn(host(Pid0),index(down,host(Z)))& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> ~ ( setIn(Z,alive)& setIn(host(Pid0),index(down,host(Z))) ) ))& (! [Z,Pid20,Pid0] :( ( ~ leq(host(Pid0),host(Z))& setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Down(Pid20),queue(host(Z))) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))& host(Pid20) = host(Z) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Z)))& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& host(Pid20) = host(Pid0)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid20),queue(host(Z))) ) ))& (! [Z,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Z))& setIn(Pid0,alive)& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid20) = host(Z)& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& ~ leq(host(Pid0),host(Z))& elem(m_Down(Pid20),queue(host(Pid0)))& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Down(Y),V) )=> ( setIn(X,alive)=> ( ~ leq(host(X),host(Y))=> ( ~ ( ( index(ldr,host(X)) = host(Y)& index(status,host(X)) = norm )| ( index(status,host(X)) = wait& host(Y) = host(index(elid,host(X))) ) )=> ( ( (! [Z] :( ( ~ leq(host(X),Z)& leq(s(zero),Z) )=> ( setIn(Z,index(down,host(X)))| Z = host(Y) ) ))& index(status,host(X)) = elec_1 )=> ( ~ leq(nbr_proc,host(X))=> (! [Z] :( host(X) != host(Z)=> (! [W0] :( host(X) = host(W0)=> ( ( ~ leq(s(host(X)),host(Z))& setIn(W0,alive) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ) ) )) )) ) ) ) ) ) )),
% 7.36/1.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.36/1.47 fof(f68,negated_conjecture,(
% 7.36/1.47 ~((! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid0),queue(host(Z))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& setIn(host(Pid0),index(down,host(Z)))& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> ~ ( setIn(Z,alive)& setIn(host(Pid0),index(down,host(Z))) ) ))& (! [Z,Pid20,Pid0] :( ( ~ leq(host(Pid0),host(Z))& setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Down(Pid20),queue(host(Z))) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))& host(Pid20) = host(Z) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Z)))& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& host(Pid20) = host(Pid0)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid20),queue(host(Z))) ) ))& (! [Z,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Z))& setIn(Pid0,alive)& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid20) = host(Z)& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& ~ leq(host(Pid0),host(Z))& elem(m_Down(Pid20),queue(host(Pid0)))& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Down(Y),V) )=> ( setIn(X,alive)=> ( ~ leq(host(X),host(Y))=> ( ~ ( ( index(ldr,host(X)) = host(Y)& index(status,host(X)) = norm )| ( index(status,host(X)) = wait& host(Y) = host(index(elid,host(X))) ) )=> ( ( (! [Z] :( ( ~ leq(host(X),Z)& leq(s(zero),Z) )=> ( setIn(Z,index(down,host(X)))| Z = host(Y) ) ))& index(status,host(X)) = elec_1 )=> ( ~ leq(nbr_proc,host(X))=> (! [Z] :( host(X) != host(Z)=> (! [W0] :( host(X) = host(W0)=> ( ( ~ leq(s(host(X)),host(Z))& setIn(W0,alive) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ) ) )) )) ) ) ) ) ) ))),
% 7.36/1.47 inference(negated_conjecture,[status(cth)],[f67])).
% 7.36/1.47 fof(f74,plain,(
% 7.36/1.47 ![X0]: (leq(s(zero),host(X0)))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f3])).
% 7.36/1.47 fof(f76,plain,(
% 7.36/1.47 ![X0]: (leq(host(X0),nbr_proc))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f5])).
% 7.36/1.47 fof(f127,plain,(
% 7.36/1.47 ![X0,X1]: (head(cons(X0,X1))=X0)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f36])).
% 7.36/1.47 fof(f133,plain,(
% 7.36/1.47 ![X0,X1]: (~q_nil=cons(X0,X1))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f42])).
% 7.36/1.47 fof(f135,plain,(
% 7.36/1.47 ![X0]: (cons(X0,q_nil)=snoc(q_nil,X0))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f44])).
% 7.36/1.47 fof(f138,plain,(
% 7.36/1.47 ![X,Y,Q]: ((~elem(X,cons(Y,Q))|(X=Y|elem(X,Q)))&(elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 7.36/1.47 inference(NNF_transformation,[status(thm)],[f47])).
% 7.36/1.47 fof(f139,plain,(
% 7.36/1.47 (![X,Y,Q]: (~elem(X,cons(Y,Q))|(X=Y|elem(X,Q))))&(![X,Y,Q]: (elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 7.36/1.47 inference(miniscoping,[status(thm)],[f138])).
% 7.36/1.47 fof(f141,plain,(
% 7.36/1.47 ![X0,X1,X2]: (elem(X0,cons(X1,X2))|~X0=X1)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f139])).
% 7.36/1.47 fof(f148,plain,(
% 7.36/1.47 ![X]: ((~pidElem(X)|(?[Y]: (X=m_Halt(Y)|X=m_Down(Y))))&(pidElem(X)|(![Y]: (~X=m_Halt(Y)&~X=m_Down(Y)))))),
% 7.36/1.47 inference(NNF_transformation,[status(thm)],[f49])).
% 7.36/1.47 fof(f149,plain,(
% 7.36/1.47 (![X]: (~pidElem(X)|((?[Y]: X=m_Halt(Y))|(?[Y]: X=m_Down(Y)))))&(![X]: (pidElem(X)|((![Y]: ~X=m_Halt(Y))&(![Y]: ~X=m_Down(Y)))))),
% 7.36/1.47 inference(miniscoping,[status(thm)],[f148])).
% 7.36/1.47 fof(f150,plain,(
% 7.36/1.47 (![X]: (~pidElem(X)|(X=m_Halt(sK0_skl(X))|X=m_Down(sK1_skl(X)))))&(![X]: (pidElem(X)|((![Y]: ~X=m_Halt(Y))&(![Y]: ~X=m_Down(Y)))))),
% 7.36/1.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl(X)),skolemize(Y,sK1_skl(X))],[f149])).
% 7.36/1.47 fof(f153,plain,(
% 7.36/1.47 ![X0,X1]: (pidElem(X0)|~X0=m_Down(X1))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f150])).
% 7.36/1.47 fof(f192,plain,(
% 7.36/1.47 ![X0]: (leq(X0,X0))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f60])).
% 7.36/1.47 fof(f193,plain,(
% 7.36/1.47 ![X0,X1]: (leq(X0,X1)|leq(X1,X0))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f61])).
% 7.36/1.47 fof(f194,plain,(
% 7.36/1.47 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 7.36/1.47 inference(NNF_transformation,[status(thm)],[f62])).
% 7.36/1.47 fof(f195,plain,(
% 7.36/1.47 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 7.36/1.47 inference(miniscoping,[status(thm)],[f194])).
% 7.36/1.47 fof(f196,plain,(
% 7.36/1.47 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f195])).
% 7.36/1.47 fof(f206,plain,(
% 7.36/1.47 ![X,Y]: ((~leq(X,s(Y))|(X=s(Y)|leq(X,Y)))&(leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 7.36/1.47 inference(NNF_transformation,[status(thm)],[f65])).
% 7.36/1.47 fof(f207,plain,(
% 7.36/1.47 (![X,Y]: (~leq(X,s(Y))|(X=s(Y)|leq(X,Y))))&(![X,Y]: (leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 7.36/1.47 inference(miniscoping,[status(thm)],[f206])).
% 7.36/1.47 fof(f208,plain,(
% 7.36/1.47 ![X0,X1]: (~leq(X0,s(X1))|X0=s(X1)|leq(X0,X1))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f207])).
% 7.36/1.47 fof(f210,plain,(
% 7.36/1.47 ![X0,X1]: (leq(X0,s(X1))|~leq(X0,X1))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f207])).
% 7.36/1.47 fof(f212,plain,(
% 7.36/1.47 (?[V,W,X,Y]: ((((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_2)|~elem(m_Ack(Z,Pid0),queue(host(Z))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~setIn(host(Pid0),index(down,host(Z))))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid0]: (((~setIn(Pid0,alive)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|(~setIn(Z,alive)|~setIn(host(Pid0),index(down,host(Z)))))))&(![Z,Pid20,Pid0]: (((((leq(host(Pid0),host(Z))|~setIn(Z,alive))|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2)|~elem(m_Down(Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20,Pid0]: (((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Pid20),queue(host(Pid0))))|~host(Pid20)=host(Z))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid20,Pid0]: (((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid20,Pid0]: (((((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Down(Pid20),queue(host(Z))))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20,Pid0]: ((((~setIn(Pid0,alive)|~host(Pid20)=host(Pid0))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|(~setIn(Z,alive)|~elem(m_Down(Pid20),queue(host(Z)))))))&(![Z,Pid0]: (((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|~index(status,host(Pid0))=elec_2)|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~leq(index(pendack,host(Z)),index(pendack,host(Pid0))))))&(![Z,Pid20,Pid0]: ((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid20)=host(Z))|~index(status,host(Pid0))=elec_2)|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid20,Pid0]: (((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|leq(host(Pid0),host(Z)))|~elem(m_Down(Pid20),queue(host(Pid0))))|~index(status,host(Pid0))=elec_1)|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(X))=cons(m_Down(Y),V))&(setIn(X,alive)&(~leq(host(X),host(Y))&(((~index(ldr,host(X))=host(Y)|~index(status,host(X))=norm)&(~index(status,host(X))=wait|~host(Y)=host(index(elid,host(X)))))&(((![Z]: ((leq(host(X),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(X)))|Z=host(Y))))&index(status,host(X))=elec_1)&(~leq(nbr_proc,host(X))&(?[Z]: (~host(X)=host(Z)&(?[W0]: (host(X)=host(W0)&((~leq(s(host(X)),host(Z))&setIn(W0,alive))&((setIn(Z,alive)&index(ldr,host(Z))=host(Z))&index(status,host(Z))=norm)))))))))))))),
% 7.36/1.47 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 7.36/1.47 fof(f213,plain,(
% 7.36/1.47 ?[X,Y]: ((((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_2)|(![Z]: ~elem(m_Ack(Z,Pid0),queue(host(Z)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~setIn(host(Pid0),index(down,host(Z))))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Pid0]: (((~setIn(Pid0,alive)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|(![Z]: (~setIn(Z,alive)|~setIn(host(Pid0),index(down,host(Z))))))))&(![Z,Pid20]: ((![Pid0]: ((((leq(host(Pid0),host(Z))|~setIn(Z,alive))|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2))|~elem(m_Down(Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z]: ((![Pid20]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))))|~host(Pid20)=host(Z)))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid20]: ((![Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid0]: (((![Pid20]: (((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Down(Pid20),queue(host(Z))))|~host(Pid0)=host(Pid20)))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Pid20]: ((![Pid0]: (((~setIn(Pid0,alive)|~host(Pid20)=host(Pid0))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0)))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid20),queue(host(Z))))))))&(![Z]: ((![Pid0]: ((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~leq(index(pendack,host(Z)),index(pendack,host(Pid0))))))&(![Z]: ((![Pid0]: ((![Pid20]: ((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid20)=host(Z)))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z]: ((![Pid0]: ((![Pid20]: (((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|leq(host(Pid0),host(Z)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~index(status,host(Pid0))=elec_1))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(?[V]: queue(host(X))=cons(m_Down(Y),V)))&(setIn(X,alive)&(~leq(host(X),host(Y))&(((~index(ldr,host(X))=host(Y)|~index(status,host(X))=norm)&(~index(status,host(X))=wait|~host(Y)=host(index(elid,host(X)))))&(((![Z]: ((leq(host(X),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(X)))|Z=host(Y))))&index(status,host(X))=elec_1)&(~leq(nbr_proc,host(X))&(?[Z]: (~host(X)=host(Z)&(?[W0]: (host(X)=host(W0)&((~leq(s(host(X)),host(Z))&setIn(W0,alive))&((setIn(Z,alive)&index(ldr,host(Z))=host(Z))&index(status,host(Z))=norm))))))))))))),
% 7.36/1.47 inference(miniscoping,[status(thm)],[f212])).
% 7.36/1.47 fof(f214,plain,(
% 7.36/1.47 ((((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_2)|(![Z]: ~elem(m_Ack(Z,Pid0),queue(host(Z)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~setIn(host(Pid0),index(down,host(Z))))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Pid0]: (((~setIn(Pid0,alive)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|(![Z]: (~setIn(Z,alive)|~setIn(host(Pid0),index(down,host(Z))))))))&(![Z,Pid20]: ((![Pid0]: ((((leq(host(Pid0),host(Z))|~setIn(Z,alive))|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2))|~elem(m_Down(Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z]: ((![Pid20]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))))|~host(Pid20)=host(Z)))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid20]: ((![Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid0]: (((![Pid20]: (((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Down(Pid20),queue(host(Z))))|~host(Pid0)=host(Pid20)))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Pid20]: ((![Pid0]: (((~setIn(Pid0,alive)|~host(Pid20)=host(Pid0))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0)))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid20),queue(host(Z))))))))&(![Z]: ((![Pid0]: ((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~leq(index(pendack,host(Z)),index(pendack,host(Pid0))))))&(![Z]: ((![Pid0]: ((![Pid20]: ((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid20)=host(Z)))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z]: ((![Pid0]: ((![Pid20]: ((((~leq(host(Pid0),sK6_skl(Pid20,Pid0,Z))&leq(s(zero),sK6_skl(Pid20,Pid0,Z)))&(~setIn(sK6_skl(Pid20,Pid0,Z),index(down,host(Pid0)))&~sK6_skl(Pid20,Pid0,Z)=host(Pid20)))|leq(host(Pid0),host(Z)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~index(status,host(Pid0))=elec_1))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(sK4_skl))=cons(m_Down(sK5_skl),sK7_skl))&(setIn(sK4_skl,alive)&(~leq(host(sK4_skl),host(sK5_skl))&(((~index(ldr,host(sK4_skl))=host(sK5_skl)|~index(status,host(sK4_skl))=norm)&(~index(status,host(sK4_skl))=wait|~host(sK5_skl)=host(index(elid,host(sK4_skl)))))&(((![Z]: ((leq(host(sK4_skl),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(sK4_skl)))|Z=host(sK5_skl))))&index(status,host(sK4_skl))=elec_1)&(~leq(nbr_proc,host(sK4_skl))&(~host(sK4_skl)=host(sK8_skl)&(host(sK4_skl)=host(sK9_skl)&((~leq(s(host(sK4_skl)),host(sK8_skl))&setIn(sK9_skl,alive))&((setIn(sK8_skl,alive)&index(ldr,host(sK8_skl))=host(sK8_skl))&index(status,host(sK8_skl))=norm))))))))))),
% 7.36/1.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(V0,sK6_skl(Pid20,Pid0,Z)),skolemize(V,sK7_skl),skolemize(Z,sK8_skl),skolemize(W0,sK9_skl)],[f213])).
% 7.36/1.47 fof(f221,plain,(
% 7.36/1.47 ![X0,X1]: (~setIn(X0,alive)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)|~setIn(X1,alive)|~setIn(host(X0),index(down,host(X1))))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f227,plain,(
% 7.36/1.47 ![X0,X1,X2]: (~setIn(X0,alive)|~host(X1)=host(X0)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)|~setIn(X2,alive)|~elem(m_Down(X1),queue(host(X2))))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f235,plain,(
% 7.36/1.47 queue(host(sK4_skl))=cons(m_Down(sK5_skl),sK7_skl)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f236,plain,(
% 7.36/1.47 setIn(sK4_skl,alive)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f237,plain,(
% 7.36/1.47 ~leq(host(sK4_skl),host(sK5_skl))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f240,plain,(
% 7.36/1.47 ![X0]: (leq(host(sK4_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK4_skl)))|X0=host(sK5_skl))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f243,plain,(
% 7.36/1.47 ~host(sK4_skl)=host(sK8_skl)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f245,plain,(
% 7.36/1.47 ~leq(s(host(sK4_skl)),host(sK8_skl))),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f247,plain,(
% 7.36/1.47 setIn(sK8_skl,alive)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f248,plain,(
% 7.36/1.47 index(ldr,host(sK8_skl))=host(sK8_skl)),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f249,plain,(
% 7.36/1.47 index(status,host(sK8_skl))=norm),
% 7.36/1.47 inference(cnf_transformation,[status(thm)],[f214])).
% 7.36/1.47 fof(f264,plain,(
% 7.36/1.47 ![X0,X1]: (elem(X0,cons(X0,X1)))),
% 7.36/1.47 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 7.36/1.47 fof(f267,plain,(
% 7.36/1.47 ![X0]: (pidElem(m_Down(X0)))),
% 7.36/1.47 inference(destructive_equality_resolution,[status(thm)],[f153])).
% 7.36/1.47 fof(f477,plain,(
% 7.36/1.47 ![X0]: (leq(host(X0),s(nbr_proc)))),
% 7.36/1.47 inference(resolution,[status(thm)],[f210,f76])).
% 7.36/1.47 fof(f599,definition,(
% 7.36/1.47 sQ33_spl <=> (index(ldr,host(sK8_skl))=host(sK8_skl))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f601,plain,(
% 7.36/1.47 ~index(ldr,host(sK8_skl))=host(sK8_skl)|sQ33_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f599])).
% 7.36/1.47 fof(f602,definition,(
% 7.36/1.47 sQ34_spl <=> (index(status,host(sK8_skl))=norm)),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f604,plain,(
% 7.36/1.47 ~index(status,host(sK8_skl))=norm|sQ34_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f602])).
% 7.36/1.47 fof(f614,plain,(
% 7.36/1.47 ~norm=norm|sQ34_spl),
% 7.36/1.47 inference(forward_demodulation,[status(thm)],[f249,f604])).
% 7.36/1.47 fof(f615,plain,(
% 7.36/1.47 $false|sQ34_spl),
% 7.36/1.47 inference(trivial_equality_resolution,[status(thm)],[f614])).
% 7.36/1.47 fof(f616,plain,(
% 7.36/1.47 sQ34_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f615])).
% 7.36/1.47 fof(f628,definition,(
% 7.36/1.47 sQ38_spl <=> (host(sK4_skl)=host(sK5_skl))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f629,plain,(
% 7.36/1.47 host(sK4_skl)=host(sK5_skl)|~sQ38_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f628])).
% 7.36/1.47 fof(f646,plain,(
% 7.36/1.47 leq(host(sK8_skl),s(host(sK4_skl)))),
% 7.36/1.47 inference(resolution,[status(thm)],[f245,f193])).
% 7.36/1.47 fof(f693,plain,(
% 7.36/1.47 ~host(sK8_skl)=host(sK8_skl)|sQ33_spl),
% 7.36/1.47 inference(forward_demodulation,[status(thm)],[f248,f601])).
% 7.36/1.47 fof(f694,plain,(
% 7.36/1.47 $false|sQ33_spl),
% 7.36/1.47 inference(trivial_equality_resolution,[status(thm)],[f693])).
% 7.36/1.47 fof(f695,plain,(
% 7.36/1.47 sQ33_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f694])).
% 7.36/1.47 fof(f1210,plain,(
% 7.36/1.47 host(sK8_skl)=s(host(sK4_skl))|leq(host(sK8_skl),host(sK4_skl))),
% 7.36/1.47 inference(resolution,[status(thm)],[f646,f208])).
% 7.36/1.47 fof(f1217,definition,(
% 7.36/1.47 sQ60_spl <=> (host(sK8_skl)=s(host(sK4_skl)))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f1218,plain,(
% 7.36/1.47 host(sK8_skl)=s(host(sK4_skl))|~sQ60_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f1217])).
% 7.36/1.47 fof(f1220,definition,(
% 7.36/1.47 sQ61_spl <=> (leq(host(sK8_skl),host(sK4_skl)))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f1221,plain,(
% 7.36/1.47 leq(host(sK8_skl),host(sK4_skl))|~sQ61_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f1220])).
% 7.36/1.47 fof(f1223,plain,(
% 7.36/1.47 sQ60_spl|sQ61_spl),
% 7.36/1.47 inference(split_clause,[status(thm)],[f1210,f1217,f1220])).
% 7.36/1.47 fof(f1230,plain,(
% 7.36/1.47 ~leq(host(sK8_skl),host(sK8_skl))|~sQ60_spl),
% 7.36/1.47 inference(backward_demodulation,[status(thm)],[f1218,f245])).
% 7.36/1.47 fof(f1237,plain,(
% 7.36/1.47 $false|~sQ60_spl),
% 7.36/1.47 inference(forward_subsumption_resolution,[status(thm)],[f1230,f192])).
% 7.36/1.47 fof(f1238,plain,(
% 7.36/1.47 ~sQ60_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f1237])).
% 7.36/1.47 fof(f1239,plain,(
% 7.36/1.47 ![X0]: (leq(host(sK4_skl),host(X0))|setIn(host(X0),index(down,host(sK4_skl)))|host(X0)=host(sK5_skl))),
% 7.36/1.47 inference(resolution,[status(thm)],[f240,f74])).
% 7.36/1.47 fof(f1372,plain,(
% 7.36/1.47 head(queue(host(sK4_skl)))=m_Down(sK5_skl)),
% 7.36/1.47 inference(paramodulation,[status(thm)],[f235,f127])).
% 7.36/1.47 fof(f1376,plain,(
% 7.36/1.47 elem(m_Down(sK5_skl),queue(host(sK4_skl)))),
% 7.36/1.47 inference(paramodulation,[status(thm)],[f235,f264])).
% 7.36/1.47 fof(f1536,plain,(
% 7.36/1.47 ~leq(host(sK4_skl),host(sK8_skl))|host(sK4_skl)=host(sK8_skl)|~sQ61_spl),
% 7.36/1.47 inference(resolution,[status(thm)],[f1221,f196])).
% 7.36/1.47 fof(f1538,definition,(
% 7.36/1.47 sQ91_spl <=> (leq(host(sK4_skl),host(sK8_skl)))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f1541,definition,(
% 7.36/1.47 sQ92_spl <=> (host(sK4_skl)=host(sK8_skl))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f1542,plain,(
% 7.36/1.47 host(sK4_skl)=host(sK8_skl)|~sQ92_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f1541])).
% 7.36/1.47 fof(f1544,plain,(
% 7.36/1.47 ~sQ91_spl|sQ92_spl|~sQ61_spl),
% 7.36/1.47 inference(split_clause,[status(thm)],[f1536,f1538,f1541,f1220])).
% 7.36/1.47 fof(f1635,plain,(
% 7.36/1.47 $false|~sQ92_spl),
% 7.36/1.47 inference(forward_subsumption_resolution,[status(thm)],[f1542,f243])).
% 7.36/1.47 fof(f1636,plain,(
% 7.36/1.47 ~sQ92_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f1635])).
% 7.36/1.47 fof(f1693,plain,(
% 7.36/1.47 ~leq(host(sK4_skl),host(sK4_skl))|~sQ38_spl),
% 7.36/1.47 inference(backward_demodulation,[status(thm)],[f629,f237])).
% 7.36/1.47 fof(f2465,plain,(
% 7.36/1.47 ![X0]: (~setIn(X0,alive)|~host(sK5_skl)=host(X0)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)|~setIn(sK4_skl,alive))),
% 7.36/1.47 inference(resolution,[status(thm)],[f1376,f227])).
% 7.36/1.47 fof(f2482,definition,(
% 7.36/1.47 sQ114_spl <=> (setIn(sK4_skl,alive))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f2484,plain,(
% 7.36/1.47 ~setIn(sK4_skl,alive)|sQ114_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f2482])).
% 7.36/1.47 fof(f2490,definition,(
% 7.36/1.47 ![X0]: (sQ116_spl <=> (~setIn(X0,alive)|~host(sK5_skl)=host(X0)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f2491,plain,(
% 7.36/1.47 ![X0]: (~setIn(X0,alive)|~host(sK5_skl)=host(X0)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)|~sQ116_spl)),
% 7.36/1.47 inference(component_clause,[status(thm)],[f2490])).
% 7.36/1.47 fof(f2493,plain,(
% 7.36/1.47 sQ116_spl|~sQ114_spl),
% 7.36/1.47 inference(split_clause,[status(thm)],[f2465,f2490,f2482])).
% 7.36/1.47 fof(f2502,plain,(
% 7.36/1.47 $false|sQ114_spl),
% 7.36/1.47 inference(forward_subsumption_resolution,[status(thm)],[f2484,f236])).
% 7.36/1.47 fof(f2503,plain,(
% 7.36/1.47 sQ114_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f2502])).
% 7.36/1.47 fof(f2617,plain,(
% 7.36/1.47 ![X0]: (leq(host(sK4_skl),host(X0))|host(X0)=host(sK5_skl)|~setIn(X0,alive)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)|~setIn(sK4_skl,alive))),
% 7.36/1.47 inference(resolution,[status(thm)],[f1239,f221])).
% 7.36/1.47 fof(f2622,definition,(
% 7.36/1.47 ![X0]: (sQ129_spl <=> (leq(host(sK4_skl),host(X0))|host(X0)=host(sK5_skl)|~setIn(X0,alive)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f2623,plain,(
% 7.36/1.47 ![X0]: (leq(host(sK4_skl),host(X0))|host(X0)=host(sK5_skl)|~setIn(X0,alive)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)|~sQ129_spl)),
% 7.36/1.47 inference(component_clause,[status(thm)],[f2622])).
% 7.36/1.47 fof(f2625,plain,(
% 7.36/1.47 sQ129_spl|~sQ114_spl),
% 7.36/1.47 inference(split_clause,[status(thm)],[f2617,f2622,f2482])).
% 7.36/1.47 fof(f2627,plain,(
% 7.36/1.47 ![X0]: (leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(status,host(X0))=norm|~index(ldr,host(X0))=host(X0)|~sQ116_spl|~sQ129_spl)),
% 7.36/1.47 inference(forward_subsumption_resolution,[status(thm)],[f2623,f2491])).
% 7.36/1.47 fof(f2651,definition,(
% 7.36/1.47 sQ132_spl <=> (s(nbr_proc)=host(sK5_skl))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f2652,plain,(
% 7.36/1.47 s(nbr_proc)=host(sK5_skl)|~sQ132_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f2651])).
% 7.36/1.47 fof(f2662,plain,(
% 7.36/1.47 ![X0]: (leq(host(X0),host(sK5_skl))|~sQ132_spl)),
% 7.36/1.47 inference(backward_demodulation,[status(thm)],[f2652,f477])).
% 7.36/1.47 fof(f2690,plain,(
% 7.36/1.47 $false|~sQ132_spl),
% 7.36/1.47 inference(backward_subsumption_resolution,[status(thm)],[f237,f2662])).
% 7.36/1.47 fof(f2692,plain,(
% 7.36/1.47 ~sQ132_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f2690])).
% 7.36/1.47 fof(f6003,plain,(
% 7.36/1.47 $false|~sQ38_spl),
% 7.36/1.47 inference(forward_subsumption_resolution,[status(thm)],[f1693,f192])).
% 7.36/1.47 fof(f6004,plain,(
% 7.36/1.47 ~sQ38_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f6003])).
% 7.36/1.47 fof(f6374,definition,(
% 7.36/1.47 sQ211_spl <=> (q_nil=snoc(q_nil,last(q_nil)))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f6375,plain,(
% 7.36/1.47 q_nil=snoc(q_nil,last(q_nil))|~sQ211_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f6374])).
% 7.36/1.47 fof(f6378,plain,(
% 7.36/1.47 q_nil=cons(last(q_nil),q_nil)|~sQ211_spl),
% 7.36/1.47 inference(forward_demodulation,[status(thm)],[f135,f6375])).
% 7.36/1.47 fof(f6379,plain,(
% 7.36/1.47 $false|~sQ211_spl),
% 7.36/1.47 inference(forward_subsumption_resolution,[status(thm)],[f6378,f133])).
% 7.36/1.47 fof(f6380,plain,(
% 7.36/1.47 ~sQ211_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f6379])).
% 7.36/1.47 fof(f6626,definition,(
% 7.36/1.47 sQ213_spl <=> (pidElem(head(queue(host(sK4_skl)))))),
% 7.36/1.47 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 7.36/1.47 fof(f6628,plain,(
% 7.36/1.47 ~pidElem(head(queue(host(sK4_skl))))|sQ213_spl),
% 7.36/1.47 inference(component_clause,[status(thm)],[f6626])).
% 7.36/1.47 fof(f6633,plain,(
% 7.36/1.47 ~pidElem(m_Down(sK5_skl))|sQ213_spl),
% 7.36/1.47 inference(forward_demodulation,[status(thm)],[f1372,f6628])).
% 7.36/1.47 fof(f6634,plain,(
% 7.36/1.47 $false|sQ213_spl),
% 7.36/1.47 inference(forward_subsumption_resolution,[status(thm)],[f6633,f267])).
% 7.36/1.47 fof(f6635,plain,(
% 7.36/1.47 sQ213_spl),
% 7.36/1.47 inference(contradiction_clause,[status(thm)],[f6634])).
% 7.36/1.47 fof(f8466,plain,(
% 7.36/1.47 leq(host(sK4_skl),host(sK8_skl))|~index(status,host(sK8_skl))=norm|~index(ldr,host(sK8_skl))=host(sK8_skl)|~sQ116_spl|~sQ129_spl),
% 7.36/1.47 inference(resolution,[status(thm)],[f2627,f247])).
% 7.36/1.48 fof(f8468,plain,(
% 7.36/1.48 sQ91_spl|~sQ34_spl|~sQ33_spl|~sQ116_spl|~sQ129_spl),
% 7.36/1.48 inference(split_clause,[status(thm)],[f8466,f1538,f602,f599,f2490,f2622])).
% 7.36/1.48 fof(f8470,plain,(
% 7.36/1.48 $false),
% 7.36/1.48 inference(sat_refutation,[status(thm)],[f616,f695,f1223,f1238,f1544,f1636,f2493,f2503,f2625,f2692,f6004,f6380,f6635,f8468])).
% 7.36/1.48 % SZS output end CNFRefutation for theBenchmark.p
% 6.22/1.51 % Elapsed time: 1.127851 seconds
% 6.22/1.51 % CPU time: 8.589444 seconds
% 6.22/1.51 % Total memory used: 162.889 MB
% 6.22/1.51 % Net memory used: 151.682 MB
%------------------------------------------------------------------------------