%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV464+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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:50:54 PM UTC 2026
% Result : Theorem 4.65s 1.20s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV464+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.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:55:17 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 4.65/1.20 % Refutation found
% 4.65/1.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.65/1.20 % SZS output start CNFRefutation for theBenchmark
% 4.65/1.20 fof(f5,axiom,(
% 4.65/1.20 (! [P] : leq(host(P),nbr_proc) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f12,axiom,(
% 4.65/1.20 (! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f16,axiom,(
% 4.65/1.20 (! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f18,axiom,(
% 4.65/1.20 (! [X,Y] : m_Down(X) != m_Halt(Y) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f48,axiom,(
% 4.65/1.20 (! [X,Y,Q] :( elem(X,snoc(Q,Y))<=> ( X = Y| elem(X,Q) ) ) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f60,axiom,(
% 4.65/1.20 (! [X] : leq(X,X) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f62,axiom,(
% 4.65/1.20 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f67,conjecture,(
% 4.65/1.20 (! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( elem(m_Down(Pid0),queue(host(Z)))=> host(Pid0) != host(Z) ))& (! [Z,Pid0] :( elem(m_Halt(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid20,Pid0] :( elem(m_Ack(Pid0,Z),queue(host(Pid20)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0))) )=> leq(host(Z),index(pendack,host(Pid0))) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = elec_1 )=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid20) = host(Z) )=> ~ ( 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(Pid0)),host(Z)) ))& (! [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] :( ( ~ 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] :( ( ~ leq(index(pendack,host(Pid0)),host(Z))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Pid20)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid0) = nbr_proc& host(Pid0) = host(Pid30)& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid30),queue(host(Z))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Pid30) = index(pendack,host(Pid0))& host(Pid20) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Ack(W,Y),V) )=> ( setIn(X,alive)=> ( ( index(elid,host(X)) = W& index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> ( ~ leq(nbr_proc,index(pendack,host(X)))=> (! [Z,W0,X0,Y0] :( s(index(pendack,host(X))) = host(Y0)=> ( host(X) != host(Y0)=> ( ( setIn(Y0,alive)& leq(nbr_proc,s(index(pendack,host(Y0))))& elem(m_Down(X0),snoc(queue(host(Y0)),m_Halt(X)))& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Halt(X)))& index(status,host(Y0)) = elec_2& host(W0) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ) ) ) )) ) ) ) )),
% 4.65/1.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.65/1.20 fof(f68,negated_conjecture,(
% 4.65/1.20 ~((! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( elem(m_Down(Pid0),queue(host(Z)))=> host(Pid0) != host(Z) ))& (! [Z,Pid0] :( elem(m_Halt(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid20,Pid0] :( elem(m_Ack(Pid0,Z),queue(host(Pid20)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0))) )=> leq(host(Z),index(pendack,host(Pid0))) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = elec_1 )=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid20) = host(Z) )=> ~ ( 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(Pid0)),host(Z)) ))& (! [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] :( ( ~ 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] :( ( ~ leq(index(pendack,host(Pid0)),host(Z))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Pid20)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid0) = nbr_proc& host(Pid0) = host(Pid30)& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid30),queue(host(Z))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Pid30) = index(pendack,host(Pid0))& host(Pid20) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Ack(W,Y),V) )=> ( setIn(X,alive)=> ( ( index(elid,host(X)) = W& index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> ( ~ leq(nbr_proc,index(pendack,host(X)))=> (! [Z,W0,X0,Y0] :( s(index(pendack,host(X))) = host(Y0)=> ( host(X) != host(Y0)=> ( ( setIn(Y0,alive)& leq(nbr_proc,s(index(pendack,host(Y0))))& elem(m_Down(X0),snoc(queue(host(Y0)),m_Halt(X)))& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Halt(X)))& index(status,host(Y0)) = elec_2& host(W0) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ) ) ) )) ) ) ) ))),
% 4.65/1.20 inference(negated_conjecture,[status(cth)],[f67])).
% 4.65/1.20 fof(f76,plain,(
% 4.65/1.20 ![X0]: (leq(host(X0),nbr_proc))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f5])).
% 4.65/1.20 fof(f83,plain,(
% 4.65/1.20 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_Halt(X2))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f12])).
% 4.65/1.20 fof(f87,plain,(
% 4.65/1.20 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_NormQ(X2))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f16])).
% 4.65/1.20 fof(f89,plain,(
% 4.65/1.20 ![X0,X1]: (~m_Down(X0)=m_Halt(X1))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f18])).
% 4.65/1.20 fof(f143,plain,(
% 4.65/1.20 ![X,Y,Q]: ((~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q)))&(elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 4.65/1.20 inference(NNF_transformation,[status(thm)],[f48])).
% 4.65/1.20 fof(f144,plain,(
% 4.65/1.20 (![X,Y,Q]: (~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q))))&(![X,Y,Q]: (elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 4.65/1.20 inference(miniscoping,[status(thm)],[f143])).
% 4.65/1.20 fof(f145,plain,(
% 4.65/1.20 ![X0,X1,X2]: (~elem(X0,snoc(X1,X2))|X0=X2|elem(X0,X1))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f144])).
% 4.65/1.20 fof(f192,plain,(
% 4.65/1.20 ![X0]: (leq(X0,X0))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f60])).
% 4.65/1.20 fof(f194,plain,(
% 4.65/1.20 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 4.65/1.20 inference(NNF_transformation,[status(thm)],[f62])).
% 4.65/1.20 fof(f195,plain,(
% 4.65/1.20 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 4.65/1.20 inference(miniscoping,[status(thm)],[f194])).
% 4.65/1.20 fof(f196,plain,(
% 4.65/1.20 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f195])).
% 4.65/1.20 fof(f212,plain,(
% 4.65/1.20 (?[V,W,X,Y]: (((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid20,Pid0]: (~elem(m_Ack(Pid0,Z),queue(host(Pid20)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|leq(host(Z),index(pendack,host(Pid0))))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_1)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid20,Pid0]: (((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid20)=host(Z))|((~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(Pid0)),host(Z)))))&(![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]: (((((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]: ((((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|~elem(m_Halt(Pid0),queue(host(Pid20))))|~index(status,host(Pid0))=elec_2)|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid30,Pid20,Pid0]: ((((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1)|(~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z)))))))&(![Z,Pid30,Pid20,Pid0]: (((((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~elem(m_Ack(Pid0,Pid30),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Pid30)=index(pendack,host(Pid0)))|~host(Pid20)=s(index(pendack,host(Pid0))))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(X))=cons(m_Ack(W,Y),V))&(setIn(X,alive)&(((index(elid,host(X))=W&index(status,host(X))=elec_2)&host(Y)=index(pendack,host(X)))&(~leq(nbr_proc,index(pendack,host(X)))&(?[Z,W0,X0,Y0]: (s(index(pendack,host(X)))=host(Y0)&(~host(X)=host(Y0)&(((((((setIn(Y0,alive)&leq(nbr_proc,s(index(pendack,host(Y0)))))&elem(m_Down(X0),snoc(queue(host(Y0)),m_Halt(X))))&elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Halt(X))))&index(status,host(Y0))=elec_2)&host(W0)=index(pendack,host(Y0)))&host(X0)=s(index(pendack,host(Y0))))&((setIn(Z,alive)&index(ldr,host(Z))=host(Z))&index(status,host(Z))=norm))))))))))),
% 4.65/1.20 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 4.65/1.20 fof(f213,plain,(
% 4.65/1.20 ?[W,X,Y]: (((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((![Pid20]: ~elem(m_Ack(Pid0,Z),queue(host(Pid20))))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|leq(host(Z),index(pendack,host(Pid0))))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_1)|(![Z]: ~elem(m_Ack(Pid0,Z),queue(host(Pid0)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z]: ((![Pid20]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid20)=host(Z)))|((~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(Pid0)),host(Z)))))&(![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]: (((((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]: (((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|(![Pid20]: ~elem(m_Halt(Pid0),queue(host(Pid20)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Pid30]: ((![Pid0]: ((((![Pid20]: ((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z))))))))&((![Pid20,Pid0]: ((![Pid30]: (((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~elem(m_Ack(Pid0,Pid30),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Pid30)=index(pendack,host(Pid0))))|~host(Pid20)=s(index(pendack,host(Pid0)))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(?[V]: queue(host(X))=cons(m_Ack(W,Y),V)))&(setIn(X,alive)&(((index(elid,host(X))=W&index(status,host(X))=elec_2)&host(Y)=index(pendack,host(X)))&(~leq(nbr_proc,index(pendack,host(X)))&(?[Y0]: (s(index(pendack,host(X)))=host(Y0)&(~host(X)=host(Y0)&((?[X0]: ((?[W0]: (((((setIn(Y0,alive)&leq(nbr_proc,s(index(pendack,host(Y0)))))&elem(m_Down(X0),snoc(queue(host(Y0)),m_Halt(X))))&elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Halt(X))))&index(status,host(Y0))=elec_2)&host(W0)=index(pendack,host(Y0))))&host(X0)=s(index(pendack,host(Y0)))))&(?[Z]: ((setIn(Z,alive)&index(ldr,host(Z))=host(Z))&index(status,host(Z))=norm))))))))))),
% 4.65/1.20 inference(miniscoping,[status(thm)],[f212])).
% 4.65/1.20 fof(f214,plain,(
% 4.65/1.20 (((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((![Pid20]: ~elem(m_Ack(Pid0,Z),queue(host(Pid20))))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|leq(host(Z),index(pendack,host(Pid0))))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_1)|(![Z]: ~elem(m_Ack(Pid0,Z),queue(host(Pid0)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z]: ((![Pid20]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid20)=host(Z)))|((~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(Pid0)),host(Z)))))&(![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]: (((((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]: (((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|(![Pid20]: ~elem(m_Halt(Pid0),queue(host(Pid20)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Pid30]: ((![Pid0]: ((((![Pid20]: (((~leq(host(Pid0),sK7_skl(Pid20,Pid0,Pid30))&leq(s(zero),sK7_skl(Pid20,Pid0,Pid30)))&(~setIn(sK7_skl(Pid20,Pid0,Pid30),index(down,host(Pid0)))&~sK7_skl(Pid20,Pid0,Pid30)=host(Pid20)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z))))))))&((![Pid20,Pid0]: ((![Pid30]: (((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~elem(m_Ack(Pid0,Pid30),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Pid30)=index(pendack,host(Pid0))))|~host(Pid20)=s(index(pendack,host(Pid0)))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(sK5_skl))=cons(m_Ack(sK4_skl,sK6_skl),sK8_skl))&(setIn(sK5_skl,alive)&(((index(elid,host(sK5_skl))=sK4_skl&index(status,host(sK5_skl))=elec_2)&host(sK6_skl)=index(pendack,host(sK5_skl)))&(~leq(nbr_proc,index(pendack,host(sK5_skl)))&(s(index(pendack,host(sK5_skl)))=host(sK9_skl)&(~host(sK5_skl)=host(sK9_skl)&(((((((setIn(sK9_skl,alive)&leq(nbr_proc,s(index(pendack,host(sK9_skl)))))&elem(m_Down(sK10_skl),snoc(queue(host(sK9_skl)),m_Halt(sK5_skl))))&elem(m_Ack(sK9_skl,sK11_skl),snoc(queue(host(sK9_skl)),m_Halt(sK5_skl))))&index(status,host(sK9_skl))=elec_2)&host(sK11_skl)=index(pendack,host(sK9_skl)))&host(sK10_skl)=s(index(pendack,host(sK9_skl))))&((setIn(sK12_skl,alive)&index(ldr,host(sK12_skl))=host(sK12_skl))&index(status,host(sK12_skl))=norm))))))))),
% 4.65/1.20 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(W,sK4_skl),skolemize(X,sK5_skl),skolemize(Y,sK6_skl),skolemize(V0,sK7_skl(Pid20,Pid0,Pid30)),skolemize(V,sK8_skl),skolemize(Y0,sK9_skl),skolemize(X0,sK10_skl),skolemize(W0,sK11_skl),skolemize(Z,sK12_skl)],[f213])).
% 4.65/1.20 fof(f223,plain,(
% 4.65/1.20 ![X0]: (~index(status,host(X0))=elec_2|~setIn(X0,alive)|index(elid,host(X0))=X0)),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f233,plain,(
% 4.65/1.20 ![X0,X1,X2,X3]: (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))|~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm)),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f235,plain,(
% 4.65/1.20 setIn(sK5_skl,alive)),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f236,plain,(
% 4.65/1.20 index(elid,host(sK5_skl))=sK4_skl),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f237,plain,(
% 4.65/1.20 index(status,host(sK5_skl))=elec_2),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f242,plain,(
% 4.65/1.20 setIn(sK9_skl,alive)),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f243,plain,(
% 4.65/1.20 leq(nbr_proc,s(index(pendack,host(sK9_skl))))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f244,plain,(
% 4.65/1.20 elem(m_Down(sK10_skl),snoc(queue(host(sK9_skl)),m_Halt(sK5_skl)))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f245,plain,(
% 4.65/1.20 elem(m_Ack(sK9_skl,sK11_skl),snoc(queue(host(sK9_skl)),m_Halt(sK5_skl)))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f246,plain,(
% 4.65/1.20 index(status,host(sK9_skl))=elec_2),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f247,plain,(
% 4.65/1.20 host(sK11_skl)=index(pendack,host(sK9_skl))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f248,plain,(
% 4.65/1.20 host(sK10_skl)=s(index(pendack,host(sK9_skl)))),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f249,plain,(
% 4.65/1.20 setIn(sK12_skl,alive)),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f250,plain,(
% 4.65/1.20 index(ldr,host(sK12_skl))=host(sK12_skl)),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f251,plain,(
% 4.65/1.20 index(status,host(sK12_skl))=norm),
% 4.65/1.20 inference(cnf_transformation,[status(thm)],[f214])).
% 4.65/1.20 fof(f252,definition,(
% 4.65/1.20 ![X0,X1,X2]: (sQ0_spl <=> (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f253,plain,(
% 4.65/1.20 ![X0,X1,X2]: (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))|~sQ0_spl)),
% 4.65/1.20 inference(component_clause,[status(thm)],[f252])).
% 4.65/1.20 fof(f255,definition,(
% 4.65/1.20 ![X3]: (sQ1_spl <=> (~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f256,plain,(
% 4.65/1.20 ![X0]: (~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ1_spl)),
% 4.65/1.20 inference(component_clause,[status(thm)],[f255])).
% 4.65/1.20 fof(f258,plain,(
% 4.65/1.20 sQ0_spl|sQ1_spl),
% 4.65/1.20 inference(split_clause,[status(thm)],[f233,f252,f255])).
% 4.65/1.20 fof(f269,plain,(
% 4.65/1.20 leq(nbr_proc,s(host(sK11_skl)))),
% 4.65/1.20 inference(backward_demodulation,[status(thm)],[f247,f243])).
% 4.65/1.20 fof(f270,plain,(
% 4.65/1.20 host(sK10_skl)=s(host(sK11_skl))),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f247,f248])).
% 4.65/1.20 fof(f271,plain,(
% 4.65/1.20 leq(nbr_proc,host(sK10_skl))),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f270,f269])).
% 4.65/1.20 fof(f401,definition,(
% 4.65/1.20 sQ15_spl <=> (index(elid,host(sK5_skl))=sK5_skl)),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f402,plain,(
% 4.65/1.20 index(elid,host(sK5_skl))=sK5_skl|~sQ15_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f401])).
% 4.65/1.20 fof(f417,plain,(
% 4.65/1.20 ~leq(host(sK10_skl),nbr_proc)|nbr_proc=host(sK10_skl)),
% 4.65/1.20 inference(resolution,[status(thm)],[f196,f271])).
% 4.65/1.20 fof(f438,definition,(
% 4.65/1.20 sQ16_spl <=> (leq(host(sK10_skl),nbr_proc))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f440,plain,(
% 4.65/1.20 ~leq(host(sK10_skl),nbr_proc)|sQ16_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f438])).
% 4.65/1.20 fof(f441,definition,(
% 4.65/1.20 sQ17_spl <=> (nbr_proc=host(sK10_skl))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f442,plain,(
% 4.65/1.20 nbr_proc=host(sK10_skl)|~sQ17_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f441])).
% 4.65/1.20 fof(f444,plain,(
% 4.65/1.20 ~sQ16_spl|sQ17_spl),
% 4.65/1.20 inference(split_clause,[status(thm)],[f417,f438,f441])).
% 4.65/1.20 fof(f454,plain,(
% 4.65/1.20 $false|sQ16_spl),
% 4.65/1.20 inference(forward_subsumption_resolution,[status(thm)],[f440,f76])).
% 4.65/1.20 fof(f455,plain,(
% 4.65/1.20 sQ16_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f454])).
% 4.65/1.20 fof(f457,plain,(
% 4.65/1.20 nbr_proc=s(host(sK11_skl))|~sQ17_spl),
% 4.65/1.20 inference(backward_demodulation,[status(thm)],[f442,f270])).
% 4.65/1.20 fof(f515,plain,(
% 4.65/1.20 ~index(status,host(sK5_skl))=elec_2|index(elid,host(sK5_skl))=sK5_skl),
% 4.65/1.20 inference(resolution,[status(thm)],[f223,f235])).
% 4.65/1.20 fof(f520,definition,(
% 4.65/1.20 sQ26_spl <=> (index(status,host(sK9_skl))=elec_2)),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f522,plain,(
% 4.65/1.20 ~index(status,host(sK9_skl))=elec_2|sQ26_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f520])).
% 4.65/1.20 fof(f524,definition,(
% 4.65/1.20 sQ27_spl <=> (index(status,host(sK5_skl))=elec_2)),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f526,plain,(
% 4.65/1.20 ~index(status,host(sK5_skl))=elec_2|sQ27_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f524])).
% 4.65/1.20 fof(f527,plain,(
% 4.65/1.20 ~sQ27_spl|sQ15_spl),
% 4.65/1.20 inference(split_clause,[status(thm)],[f515,f524,f401])).
% 4.65/1.20 fof(f533,plain,(
% 4.65/1.20 elem(m_Ack(sK9_skl,sK11_skl),snoc(queue(host(sK9_skl)),m_Halt(sK4_skl)))|~sQ15_spl),
% 4.65/1.20 inference(backward_demodulation,[status(thm)],[f537,f245])).
% 4.65/1.20 fof(f534,plain,(
% 4.65/1.20 elem(m_Down(sK10_skl),snoc(queue(host(sK9_skl)),m_Halt(sK4_skl)))|~sQ15_spl),
% 4.65/1.20 inference(backward_demodulation,[status(thm)],[f537,f244])).
% 4.65/1.20 fof(f537,plain,(
% 4.65/1.20 sK4_skl=sK5_skl|~sQ15_spl),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f236,f402])).
% 4.65/1.20 fof(f566,plain,(
% 4.65/1.20 $false|sQ27_spl),
% 4.65/1.20 inference(forward_subsumption_resolution,[status(thm)],[f237,f526])).
% 4.65/1.20 fof(f567,plain,(
% 4.65/1.20 sQ27_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f566])).
% 4.65/1.20 fof(f647,definition,(
% 4.65/1.20 sQ37_spl <=> (index(ldr,host(sK12_skl))=host(sK12_skl))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f649,plain,(
% 4.65/1.20 ~index(ldr,host(sK12_skl))=host(sK12_skl)|sQ37_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f647])).
% 4.65/1.20 fof(f650,definition,(
% 4.65/1.20 sQ38_spl <=> (index(status,host(sK12_skl))=norm)),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f652,plain,(
% 4.65/1.20 ~index(status,host(sK12_skl))=norm|sQ38_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f650])).
% 4.65/1.20 fof(f669,plain,(
% 4.65/1.20 ~norm=norm|sQ38_spl),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f251,f652])).
% 4.65/1.20 fof(f670,plain,(
% 4.65/1.20 $false|sQ38_spl),
% 4.65/1.20 inference(trivial_equality_resolution,[status(thm)],[f669])).
% 4.65/1.20 fof(f671,plain,(
% 4.65/1.20 sQ38_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f670])).
% 4.65/1.20 fof(f672,plain,(
% 4.65/1.20 ~host(sK12_skl)=host(sK12_skl)|sQ37_spl),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f250,f649])).
% 4.65/1.20 fof(f673,plain,(
% 4.65/1.20 $false|sQ37_spl),
% 4.65/1.20 inference(trivial_equality_resolution,[status(thm)],[f672])).
% 4.65/1.20 fof(f674,plain,(
% 4.65/1.20 sQ37_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f673])).
% 4.65/1.20 fof(f798,plain,(
% 4.65/1.20 ~elec_2=elec_2|sQ26_spl),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f246,f522])).
% 4.65/1.20 fof(f799,plain,(
% 4.65/1.20 $false|sQ26_spl),
% 4.65/1.20 inference(trivial_equality_resolution,[status(thm)],[f798])).
% 4.65/1.20 fof(f800,plain,(
% 4.65/1.20 sQ26_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f799])).
% 4.65/1.20 fof(f1004,definition,(
% 4.65/1.20 sQ74_spl <=> (setIn(sK9_skl,alive))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f1006,plain,(
% 4.65/1.20 ~setIn(sK9_skl,alive)|sQ74_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f1004])).
% 4.65/1.20 fof(f1012,plain,(
% 4.65/1.20 $false|sQ74_spl),
% 4.65/1.20 inference(forward_subsumption_resolution,[status(thm)],[f1006,f242])).
% 4.65/1.20 fof(f1013,plain,(
% 4.65/1.20 sQ74_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f1012])).
% 4.65/1.20 fof(f1037,definition,(
% 4.65/1.20 ![X0]: (sQ81_spl <=> (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=s(index(pendack,host(sK9_skl)))))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f1038,plain,(
% 4.65/1.20 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=s(index(pendack,host(sK9_skl)))|~sQ81_spl)),
% 4.65/1.20 inference(component_clause,[status(thm)],[f1037])).
% 4.65/1.20 fof(f1059,plain,(
% 4.65/1.20 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=s(host(sK11_skl))|~sQ81_spl)),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f247,f1038])).
% 4.65/1.20 fof(f1060,plain,(
% 4.65/1.20 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=nbr_proc|~sQ17_spl|~sQ81_spl)),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f457,f1059])).
% 4.65/1.20 fof(f1087,plain,(
% 4.65/1.20 m_Ack(sK9_skl,sK11_skl)=m_Halt(sK4_skl)|elem(m_Ack(sK9_skl,sK11_skl),queue(host(sK9_skl)))|~sQ15_spl),
% 4.65/1.20 inference(resolution,[status(thm)],[f533,f145])).
% 4.65/1.20 fof(f1092,definition,(
% 4.65/1.20 sQ85_spl <=> (m_Ack(sK9_skl,sK11_skl)=m_Halt(sK4_skl))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f1093,plain,(
% 4.65/1.20 m_Ack(sK9_skl,sK11_skl)=m_Halt(sK4_skl)|~sQ85_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f1092])).
% 4.65/1.20 fof(f1095,definition,(
% 4.65/1.20 sQ86_spl <=> (elem(m_Ack(sK9_skl,sK11_skl),queue(host(sK9_skl))))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f1096,plain,(
% 4.65/1.20 elem(m_Ack(sK9_skl,sK11_skl),queue(host(sK9_skl)))|~sQ86_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f1095])).
% 4.65/1.20 fof(f1098,plain,(
% 4.65/1.20 sQ85_spl|sQ86_spl|~sQ15_spl),
% 4.65/1.20 inference(split_clause,[status(thm)],[f1087,f1092,f1095,f401])).
% 4.65/1.20 fof(f1110,plain,(
% 4.65/1.20 $false|~sQ85_spl),
% 4.65/1.20 inference(forward_subsumption_resolution,[status(thm)],[f1093,f83])).
% 4.65/1.20 fof(f1111,plain,(
% 4.65/1.20 ~sQ85_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f1110])).
% 4.65/1.20 fof(f1124,plain,(
% 4.65/1.20 m_Down(sK10_skl)=m_Halt(sK4_skl)|elem(m_Down(sK10_skl),queue(host(sK9_skl)))|~sQ15_spl),
% 4.65/1.20 inference(resolution,[status(thm)],[f534,f145])).
% 4.65/1.20 fof(f1130,definition,(
% 4.65/1.20 sQ90_spl <=> (m_Down(sK10_skl)=m_Halt(sK4_skl))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f1131,plain,(
% 4.65/1.20 m_Down(sK10_skl)=m_Halt(sK4_skl)|~sQ90_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f1130])).
% 4.65/1.20 fof(f1133,definition,(
% 4.65/1.20 sQ91_spl <=> (elem(m_Down(sK10_skl),queue(host(sK9_skl))))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f1134,plain,(
% 4.65/1.20 elem(m_Down(sK10_skl),queue(host(sK9_skl)))|~sQ91_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f1133])).
% 4.65/1.20 fof(f1136,plain,(
% 4.65/1.20 sQ90_spl|sQ91_spl|~sQ15_spl),
% 4.65/1.20 inference(split_clause,[status(thm)],[f1124,f1130,f1133,f401])).
% 4.65/1.20 fof(f1150,plain,(
% 4.65/1.20 $false|~sQ90_spl),
% 4.65/1.20 inference(forward_subsumption_resolution,[status(thm)],[f1131,f89])).
% 4.65/1.20 fof(f1151,plain,(
% 4.65/1.20 ~sQ90_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f1150])).
% 4.65/1.20 fof(f3491,plain,(
% 4.65/1.20 ~index(ldr,host(sK12_skl))=host(sK12_skl)|~index(status,host(sK12_skl))=norm|~sQ1_spl),
% 4.65/1.20 inference(resolution,[status(thm)],[f256,f249])).
% 4.65/1.20 fof(f3494,plain,(
% 4.65/1.20 ~sQ37_spl|~sQ38_spl|~sQ1_spl),
% 4.65/1.20 inference(split_clause,[status(thm)],[f3491,f647,f650,f255])).
% 4.65/1.20 fof(f4902,definition,(
% 4.65/1.20 sQ189_spl <=> (leq(nbr_proc,s(index(pendack,host(sK9_skl)))))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f4904,plain,(
% 4.65/1.20 ~leq(nbr_proc,s(index(pendack,host(sK9_skl))))|sQ189_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f4902])).
% 4.65/1.20 fof(f4975,plain,(
% 4.65/1.20 ~leq(nbr_proc,s(host(sK11_skl)))|sQ189_spl),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f247,f4904])).
% 4.65/1.20 fof(f4976,plain,(
% 4.65/1.20 ~leq(nbr_proc,nbr_proc)|~sQ17_spl|sQ189_spl),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f457,f4975])).
% 4.65/1.20 fof(f4977,plain,(
% 4.65/1.20 $false|~sQ17_spl|sQ189_spl),
% 4.65/1.20 inference(forward_subsumption_resolution,[status(thm)],[f4976,f192])).
% 4.65/1.20 fof(f4978,plain,(
% 4.65/1.20 ~sQ17_spl|sQ189_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f4977])).
% 4.65/1.20 fof(f5070,plain,(
% 4.65/1.20 ![X0]: (~setIn(sK9_skl,alive)|~elem(m_Down(X0),queue(host(sK9_skl)))|~leq(nbr_proc,s(index(pendack,host(sK9_skl))))|~index(status,host(sK9_skl))=elec_2|~host(sK11_skl)=index(pendack,host(sK9_skl))|~host(X0)=s(index(pendack,host(sK9_skl)))|~sQ86_spl|~sQ0_spl)),
% 4.65/1.20 inference(resolution,[status(thm)],[f1096,f253])).
% 4.65/1.20 fof(f5075,definition,(
% 4.65/1.20 sQ208_spl <=> (host(sK11_skl)=index(pendack,host(sK9_skl)))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f5077,plain,(
% 4.65/1.20 ~host(sK11_skl)=index(pendack,host(sK9_skl))|sQ208_spl),
% 4.65/1.20 inference(component_clause,[status(thm)],[f5075])).
% 4.65/1.20 fof(f5088,plain,(
% 4.65/1.20 ~sQ74_spl|sQ81_spl|~sQ189_spl|~sQ26_spl|~sQ208_spl|~sQ86_spl|~sQ0_spl),
% 4.65/1.20 inference(split_clause,[status(thm)],[f5070,f1004,f1037,f4902,f520,f5075,f1095,f252])).
% 4.65/1.20 fof(f5097,plain,(
% 4.65/1.20 ~host(sK11_skl)=host(sK11_skl)|sQ208_spl),
% 4.65/1.20 inference(forward_demodulation,[status(thm)],[f247,f5077])).
% 4.65/1.20 fof(f5098,plain,(
% 4.65/1.20 $false|sQ208_spl),
% 4.65/1.20 inference(trivial_equality_resolution,[status(thm)],[f5097])).
% 4.65/1.20 fof(f5099,plain,(
% 4.65/1.20 sQ208_spl),
% 4.65/1.20 inference(contradiction_clause,[status(thm)],[f5098])).
% 4.65/1.20 fof(f5119,definition,(
% 4.65/1.20 ![X0]: (sQ215_spl <=> (m_Ack(sK9_skl,sK11_skl)=X0))),
% 4.65/1.20 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 4.65/1.20 fof(f5120,plain,(
% 4.65/1.20 ![X0]: (m_Ack(sK9_skl,sK11_skl)=X0|~sQ215_spl)),
% 4.65/1.20 inference(component_clause,[status(thm)],[f5119])).
% 4.65/1.20 fof(f5159,plain,(
% 4.65/1.21 $false|~sQ215_spl),
% 4.65/1.21 inference(resolution,[status(thm)],[f5120,f87])).
% 4.65/1.21 fof(f5191,plain,(
% 4.65/1.21 ~sQ215_spl),
% 4.65/1.21 inference(contradiction_clause,[status(thm)],[f5159])).
% 4.65/1.21 fof(f5211,plain,(
% 4.65/1.21 ~host(sK10_skl)=nbr_proc|~sQ17_spl|~sQ81_spl|~sQ91_spl),
% 4.65/1.21 inference(resolution,[status(thm)],[f1060,f1134])).
% 4.65/1.21 fof(f5212,plain,(
% 4.65/1.21 ~nbr_proc=nbr_proc|~sQ17_spl|~sQ81_spl|~sQ91_spl),
% 4.65/1.21 inference(forward_demodulation,[status(thm)],[f442,f5211])).
% 4.65/1.21 fof(f5213,plain,(
% 4.65/1.21 $false|~sQ17_spl|~sQ81_spl|~sQ91_spl),
% 4.65/1.21 inference(trivial_equality_resolution,[status(thm)],[f5212])).
% 4.65/1.21 fof(f5214,plain,(
% 4.65/1.21 ~sQ17_spl|~sQ81_spl|~sQ91_spl),
% 4.65/1.21 inference(contradiction_clause,[status(thm)],[f5213])).
% 4.65/1.21 fof(f5215,plain,(
% 4.65/1.21 $false),
% 4.65/1.21 inference(sat_refutation,[status(thm)],[f258,f444,f455,f527,f567,f671,f674,f800,f1013,f1098,f1111,f1136,f1151,f3494,f4978,f5088,f5099,f5191,f5214])).
% 4.65/1.21 % SZS output end CNFRefutation for theBenchmark.p
% 5.79/1.23 % Elapsed time: 0.861368 seconds
% 5.79/1.23 % CPU time: 6.412693 seconds
% 5.79/1.23 % Total memory used: 174.495 MB
% 5.79/1.23 % Net memory used: 162.528 MB
%------------------------------------------------------------------------------