%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV466+1 : 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 : 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 21.68s 13.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV466+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/10.43 % Computer : n004.cluster.edu
% 0.13/10.43 % Model : x86_64 x86_64
% 0.13/10.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.43 % Memory : 8046.5625MB
% 0.13/10.43 % OS : Linux 6.8.0-71-generic
% 0.13/10.43 % CPULimit : 300
% 0.13/10.43 % WCLimit : 300
% 0.13/10.43 % DateTime : Mon Sep 21 08:52:45 UTC 2026
% 0.13/10.44 % CPUTime :
% 0.13/10.46 % Drodi V4.1.1
% 21.68/13.31 % Refutation found
% 21.68/13.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 21.68/13.31 % SZS output start CNFRefutation for theBenchmark
% 21.68/13.31 fof(f5,axiom,(
% 21.68/13.31 (! [P] : leq(host(P),nbr_proc) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f15,axiom,(
% 21.68/13.31 (! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f47,axiom,(
% 21.68/13.31 (! [X,Y,Q] :( elem(X,cons(Y,Q))<=> ( X = Y| elem(X,Q) ) ) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f48,axiom,(
% 21.68/13.31 (! [X,Y,Q] :( elem(X,snoc(Q,Y))<=> ( X = Y| elem(X,Q) ) ) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f59,axiom,(
% 21.68/13.31 (! [X] : ~ leq(s(X),X) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f61,axiom,(
% 21.68/13.31 (! [X,Y] :( leq(X,Y)| leq(Y,X) ) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f62,axiom,(
% 21.68/13.31 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f65,axiom,(
% 21.68/13.31 (! [X,Y] :( leq(X,s(Y))<=> ( X = s(Y)| leq(X,Y) ) ) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f67,conjecture,(
% 21.68/13.31 (! [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_Down(Y),V) )=> ( setIn(X,alive)=> ( leq(host(X),host(Y))=> ( ( index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> ( leq(nbr_proc,index(pendack,host(X)))=> (! [Z] :( setIn(host(Z),index(acks,host(X)))=> (! [V0] :( host(X) = host(V0)=> (! [W0,X0,Y0] :( host(Z) = 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_Ldr(X)))& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))& index(status,host(Y0)) = elec_2& host(W0) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(V0,alive)& host(X) = host(V0) ) ) ) ) )) )) )) ) ) ) ) )),
% 21.68/13.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.68/13.31 fof(f68,negated_conjecture,(
% 21.68/13.31 ~((! [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_Down(Y),V) )=> ( setIn(X,alive)=> ( leq(host(X),host(Y))=> ( ( index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> ( leq(nbr_proc,index(pendack,host(X)))=> (! [Z] :( setIn(host(Z),index(acks,host(X)))=> (! [V0] :( host(X) = host(V0)=> (! [W0,X0,Y0] :( host(Z) = 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_Ldr(X)))& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))& index(status,host(Y0)) = elec_2& host(W0) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(V0,alive)& host(X) = host(V0) ) ) ) ) )) )) )) ) ) ) ) ))),
% 21.68/13.31 inference(negated_conjecture,[status(cth)],[f67])).
% 21.68/13.31 fof(f76,plain,(
% 21.68/13.31 ![X0]: (leq(host(X0),nbr_proc))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f5])).
% 21.68/13.31 fof(f86,plain,(
% 21.68/13.31 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_Ldr(X2))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f15])).
% 21.68/13.31 fof(f138,plain,(
% 21.68/13.31 ![X,Y,Q]: ((~elem(X,cons(Y,Q))|(X=Y|elem(X,Q)))&(elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 21.68/13.31 inference(NNF_transformation,[status(thm)],[f47])).
% 21.68/13.31 fof(f139,plain,(
% 21.68/13.31 (![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))))),
% 21.68/13.31 inference(miniscoping,[status(thm)],[f138])).
% 21.68/13.31 fof(f141,plain,(
% 21.68/13.31 ![X0,X1,X2]: (elem(X0,cons(X1,X2))|~X0=X1)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f139])).
% 21.68/13.31 fof(f143,plain,(
% 21.68/13.31 ![X,Y,Q]: ((~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q)))&(elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 21.68/13.31 inference(NNF_transformation,[status(thm)],[f48])).
% 21.68/13.31 fof(f144,plain,(
% 21.68/13.31 (![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))))),
% 21.68/13.31 inference(miniscoping,[status(thm)],[f143])).
% 21.68/13.31 fof(f145,plain,(
% 21.68/13.31 ![X0,X1,X2]: (~elem(X0,snoc(X1,X2))|X0=X2|elem(X0,X1))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f144])).
% 21.68/13.31 fof(f191,plain,(
% 21.68/13.31 ![X0]: (~leq(s(X0),X0))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f59])).
% 21.68/13.31 fof(f193,plain,(
% 21.68/13.31 ![X0,X1]: (leq(X0,X1)|leq(X1,X0))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f61])).
% 21.68/13.31 fof(f194,plain,(
% 21.68/13.31 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 21.68/13.31 inference(NNF_transformation,[status(thm)],[f62])).
% 21.68/13.31 fof(f195,plain,(
% 21.68/13.31 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 21.68/13.31 inference(miniscoping,[status(thm)],[f194])).
% 21.68/13.31 fof(f196,plain,(
% 21.68/13.31 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f195])).
% 21.68/13.31 fof(f206,plain,(
% 21.68/13.31 ![X,Y]: ((~leq(X,s(Y))|(X=s(Y)|leq(X,Y)))&(leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 21.68/13.31 inference(NNF_transformation,[status(thm)],[f65])).
% 21.68/13.31 fof(f207,plain,(
% 21.68/13.31 (![X,Y]: (~leq(X,s(Y))|(X=s(Y)|leq(X,Y))))&(![X,Y]: (leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 21.68/13.31 inference(miniscoping,[status(thm)],[f206])).
% 21.68/13.31 fof(f208,plain,(
% 21.68/13.31 ![X0,X1]: (~leq(X0,s(X1))|X0=s(X1)|leq(X0,X1))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f207])).
% 21.68/13.31 fof(f212,plain,(
% 21.68/13.31 (?[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_Down(Y),V))&(setIn(X,alive)&(leq(host(X),host(Y))&((index(status,host(X))=elec_2&host(Y)=index(pendack,host(X)))&(leq(nbr_proc,index(pendack,host(X)))&(?[Z]: (setIn(host(Z),index(acks,host(X)))&(?[V0]: (host(X)=host(V0)&(?[W0,X0,Y0]: (host(Z)=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_Ldr(X))))&elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X))))&index(status,host(Y0))=elec_2)&host(W0)=index(pendack,host(Y0)))&host(X0)=s(index(pendack,host(Y0))))&(setIn(V0,alive)&host(X)=host(V0))))))))))))))))),
% 21.68/13.31 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 21.68/13.31 fof(f213,plain,(
% 21.68/13.31 ?[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_Down(Y),V)))&(setIn(X,alive)&(leq(host(X),host(Y))&((index(status,host(X))=elec_2&host(Y)=index(pendack,host(X)))&(leq(nbr_proc,index(pendack,host(X)))&(?[Z]: (setIn(host(Z),index(acks,host(X)))&(?[V0]: (host(X)=host(V0)&(?[Y0]: (host(Z)=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_Ldr(X))))&elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X))))&index(status,host(Y0))=elec_2)&host(W0)=index(pendack,host(Y0))))&host(X0)=s(index(pendack,host(Y0)))))&(setIn(V0,alive)&host(X)=host(V0)))))))))))))))),
% 21.68/13.31 inference(miniscoping,[status(thm)],[f212])).
% 21.68/13.31 fof(f214,plain,(
% 21.68/13.31 (((((((((((((((((![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),sK6_skl(Pid20,Pid0,Pid30))&leq(s(zero),sK6_skl(Pid20,Pid0,Pid30)))&(~setIn(sK6_skl(Pid20,Pid0,Pid30),index(down,host(Pid0)))&~sK6_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(sK4_skl))=cons(m_Down(sK5_skl),sK7_skl))&(setIn(sK4_skl,alive)&(leq(host(sK4_skl),host(sK5_skl))&((index(status,host(sK4_skl))=elec_2&host(sK5_skl)=index(pendack,host(sK4_skl)))&(leq(nbr_proc,index(pendack,host(sK4_skl)))&(setIn(host(sK8_skl),index(acks,host(sK4_skl)))&(host(sK4_skl)=host(sK9_skl)&(host(sK8_skl)=host(sK10_skl)&(~host(sK4_skl)=host(sK10_skl)&(((((((setIn(sK10_skl,alive)&leq(nbr_proc,s(index(pendack,host(sK10_skl)))))&elem(m_Down(sK11_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl))))&elem(m_Ack(sK10_skl,sK12_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl))))&index(status,host(sK10_skl))=elec_2)&host(sK12_skl)=index(pendack,host(sK10_skl)))&host(sK11_skl)=s(index(pendack,host(sK10_skl))))&(setIn(sK9_skl,alive)&host(sK4_skl)=host(sK9_skl))))))))))))),
% 21.68/13.31 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(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(V0,sK6_skl(Pid20,Pid0,Pid30)),skolemize(V,sK7_skl),skolemize(Z,sK8_skl),skolemize(V0,sK9_skl),skolemize(Y0,sK10_skl),skolemize(X0,sK11_skl),skolemize(W0,sK12_skl)],[f213])).
% 21.68/13.31 fof(f216,plain,(
% 21.68/13.31 ![X0,X1]: (~elem(m_Down(X0),queue(host(X1)))|~host(X0)=host(X1))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f225,plain,(
% 21.68/13.31 ![X0,X1]: (leq(host(X0),host(X1))|~setIn(X0,alive)|~setIn(X1,alive)|~index(status,host(X0))=elec_2|~index(status,host(X1))=elec_2|leq(index(pendack,host(X1)),host(X0)))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f226,plain,(
% 21.68/13.31 ![X0,X1,X2]: (~setIn(X0,alive)|~setIn(X1,alive)|~host(X1)=host(X2)|~index(status,host(X0))=elec_2|~index(status,host(X1))=elec_2|~elem(m_Ack(X0,X2),queue(host(X0))))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f227,plain,(
% 21.68/13.31 ![X0,X1]: (leq(host(X0),host(X1))|~setIn(X0,alive)|~setIn(X1,alive)|~index(status,host(X0))=elec_2|~index(status,host(X1))=elec_2|~leq(index(pendack,host(X0)),index(pendack,host(X1))))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f234,plain,(
% 21.68/13.31 queue(host(sK4_skl))=cons(m_Down(sK5_skl),sK7_skl)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f235,plain,(
% 21.68/13.31 setIn(sK4_skl,alive)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f237,plain,(
% 21.68/13.31 index(status,host(sK4_skl))=elec_2),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f238,plain,(
% 21.68/13.31 host(sK5_skl)=index(pendack,host(sK4_skl))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f239,plain,(
% 21.68/13.31 leq(nbr_proc,index(pendack,host(sK4_skl)))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f241,plain,(
% 21.68/13.31 host(sK4_skl)=host(sK9_skl)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f242,plain,(
% 21.68/13.31 host(sK8_skl)=host(sK10_skl)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f243,plain,(
% 21.68/13.31 ~host(sK4_skl)=host(sK10_skl)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f244,plain,(
% 21.68/13.31 setIn(sK10_skl,alive)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f245,plain,(
% 21.68/13.31 leq(nbr_proc,s(index(pendack,host(sK10_skl))))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f247,plain,(
% 21.68/13.31 elem(m_Ack(sK10_skl,sK12_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl)))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f248,plain,(
% 21.68/13.31 index(status,host(sK10_skl))=elec_2),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f249,plain,(
% 21.68/13.31 host(sK12_skl)=index(pendack,host(sK10_skl))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f250,plain,(
% 21.68/13.31 host(sK11_skl)=s(index(pendack,host(sK10_skl)))),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f251,plain,(
% 21.68/13.31 setIn(sK9_skl,alive)),
% 21.68/13.31 inference(cnf_transformation,[status(thm)],[f214])).
% 21.68/13.31 fof(f253,plain,(
% 21.68/13.31 ![X0,X1]: (elem(X0,cons(X0,X1)))),
% 21.68/13.31 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 21.68/13.31 fof(f430,plain,(
% 21.68/13.31 ~host(sK4_skl)=host(sK8_skl)),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f243])).
% 21.68/13.31 fof(f432,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK9_skl),host(X0))|~setIn(X0,alive)|~index(status,host(sK9_skl))=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK9_skl)))),
% 21.68/13.31 inference(resolution,[status(thm)],[f225,f251])).
% 21.68/13.31 fof(f448,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(status,host(sK9_skl))=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK9_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f241,f432])).
% 21.68/13.31 fof(f449,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(status,host(sK4_skl))=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK9_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f241,f448])).
% 21.68/13.31 fof(f450,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(status,host(sK4_skl))=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK4_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f241,f449])).
% 21.68/13.31 fof(f469,plain,(
% 21.68/13.31 ![X0,X1]: (~setIn(X0,alive)|~host(sK9_skl)=host(X1)|~index(status,host(X0))=elec_2|~index(status,host(sK9_skl))=elec_2|~elem(m_Ack(X0,X1),queue(host(X0))))),
% 21.68/13.31 inference(resolution,[status(thm)],[f226,f251])).
% 21.68/13.31 fof(f474,plain,(
% 21.68/13.31 ![X0,X1]: (~setIn(X0,alive)|~host(sK4_skl)=host(X1)|~index(status,host(X0))=elec_2|~index(status,host(sK9_skl))=elec_2|~elem(m_Ack(X0,X1),queue(host(X0))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f241,f469])).
% 21.68/13.31 fof(f475,plain,(
% 21.68/13.31 ![X0,X1]: (~setIn(X0,alive)|~host(sK4_skl)=host(X1)|~index(status,host(X0))=elec_2|~index(status,host(sK4_skl))=elec_2|~elem(m_Ack(X0,X1),queue(host(X0))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f241,f474])).
% 21.68/13.31 fof(f558,plain,(
% 21.68/13.31 ![X0,X1]: (leq(host(X0),host(X1))|~setIn(X0,alive)|~setIn(X1,alive)|~index(status,host(X0))=elec_2|~index(status,host(X1))=elec_2|leq(index(pendack,host(X1)),index(pendack,host(X0))))),
% 21.68/13.31 inference(resolution,[status(thm)],[f227,f193])).
% 21.68/13.31 fof(f795,plain,(
% 21.68/13.31 elem(m_Down(sK5_skl),queue(host(sK4_skl)))),
% 21.68/13.31 inference(paramodulation,[status(thm)],[f234,f253])).
% 21.68/13.31 fof(f815,plain,(
% 21.68/13.31 leq(nbr_proc,host(sK5_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f238,f239])).
% 21.68/13.31 fof(f820,plain,(
% 21.68/13.31 ~leq(host(sK5_skl),nbr_proc)|host(sK5_skl)=nbr_proc),
% 21.68/13.31 inference(resolution,[status(thm)],[f815,f196])).
% 21.68/13.31 fof(f822,plain,(
% 21.68/13.31 host(sK5_skl)=nbr_proc),
% 21.68/13.31 inference(forward_subsumption_resolution,[status(thm)],[f820,f76])).
% 21.68/13.31 fof(f824,plain,(
% 21.68/13.31 leq(nbr_proc,s(index(pendack,host(sK8_skl))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f245])).
% 21.68/13.31 fof(f847,plain,(
% 21.68/13.31 elem(m_Ack(sK10_skl,sK12_skl),snoc(queue(host(sK8_skl)),m_Ldr(sK4_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f247])).
% 21.68/13.31 fof(f848,plain,(
% 21.68/13.31 m_Ack(sK10_skl,sK12_skl)=m_Ldr(sK4_skl)|elem(m_Ack(sK10_skl,sK12_skl),queue(host(sK8_skl)))),
% 21.68/13.31 inference(resolution,[status(thm)],[f847,f145])).
% 21.68/13.31 fof(f853,plain,(
% 21.68/13.31 elem(m_Ack(sK10_skl,sK12_skl),queue(host(sK8_skl)))),
% 21.68/13.31 inference(forward_subsumption_resolution,[status(thm)],[f848,f86])).
% 21.68/13.31 fof(f854,plain,(
% 21.68/13.31 index(status,host(sK8_skl))=elec_2),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f248])).
% 21.68/13.31 fof(f856,plain,(
% 21.68/13.31 nbr_proc=index(pendack,host(sK4_skl))),
% 21.68/13.31 inference(backward_demodulation,[status(thm)],[f822,f238])).
% 21.68/13.31 fof(f929,plain,(
% 21.68/13.31 leq(nbr_proc,s(host(sK12_skl)))),
% 21.68/13.31 inference(backward_demodulation,[status(thm)],[f930,f824])).
% 21.68/13.31 fof(f930,plain,(
% 21.68/13.31 host(sK12_skl)=index(pendack,host(sK8_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f249])).
% 21.68/13.31 fof(f942,plain,(
% 21.68/13.31 host(sK11_skl)=s(index(pendack,host(sK8_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f250])).
% 21.68/13.31 fof(f943,plain,(
% 21.68/13.31 host(sK11_skl)=s(host(sK12_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f930,f942])).
% 21.68/13.31 fof(f949,plain,(
% 21.68/13.31 ![X0]: (~leq(X0,host(sK11_skl))|X0=s(host(sK12_skl))|leq(X0,host(sK12_skl)))),
% 21.68/13.31 inference(paramodulation,[status(thm)],[f943,f208])).
% 21.68/13.31 fof(f956,plain,(
% 21.68/13.31 ![X0]: (~leq(X0,host(sK11_skl))|X0=host(sK11_skl)|leq(X0,host(sK12_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f943,f949])).
% 21.68/13.31 fof(f971,plain,(
% 21.68/13.31 leq(nbr_proc,host(sK11_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f943,f929])).
% 21.68/13.31 fof(f976,plain,(
% 21.68/13.31 ~leq(host(sK11_skl),nbr_proc)|host(sK11_skl)=nbr_proc),
% 21.68/13.31 inference(resolution,[status(thm)],[f971,f196])).
% 21.68/13.31 fof(f978,plain,(
% 21.68/13.31 host(sK11_skl)=nbr_proc),
% 21.68/13.31 inference(forward_subsumption_resolution,[status(thm)],[f976,f76])).
% 21.68/13.31 fof(f1004,plain,(
% 21.68/13.31 nbr_proc=s(host(sK12_skl))),
% 21.68/13.31 inference(backward_demodulation,[status(thm)],[f978,f943])).
% 21.68/13.31 fof(f1084,plain,(
% 21.68/13.31 ~leq(nbr_proc,host(sK12_skl))),
% 21.68/13.31 inference(paramodulation,[status(thm)],[f1004,f191])).
% 21.68/13.31 fof(f1459,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~elec_2=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK4_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f237,f450])).
% 21.68/13.31 fof(f1460,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK4_skl)))),
% 21.68/13.31 inference(trivial_equality_resolution,[status(thm)],[f1459])).
% 21.68/13.31 fof(f1461,plain,(
% 21.68/13.31 leq(host(sK4_skl),host(sK10_skl))|~index(status,host(sK10_skl))=elec_2|leq(index(pendack,host(sK10_skl)),host(sK4_skl))),
% 21.68/13.31 inference(resolution,[status(thm)],[f1460,f244])).
% 21.68/13.31 fof(f1463,plain,(
% 21.68/13.31 leq(host(sK4_skl),host(sK8_skl))|~index(status,host(sK10_skl))=elec_2|leq(index(pendack,host(sK10_skl)),host(sK4_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f1461])).
% 21.68/13.31 fof(f1464,plain,(
% 21.68/13.31 leq(host(sK4_skl),host(sK8_skl))|~index(status,host(sK8_skl))=elec_2|leq(index(pendack,host(sK10_skl)),host(sK4_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f1463])).
% 21.68/13.31 fof(f1465,plain,(
% 21.68/13.31 leq(host(sK4_skl),host(sK8_skl))|~elec_2=elec_2|leq(index(pendack,host(sK10_skl)),host(sK4_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f854,f1464])).
% 21.68/13.31 fof(f1466,plain,(
% 21.68/13.31 leq(host(sK4_skl),host(sK8_skl))|~elec_2=elec_2|leq(index(pendack,host(sK8_skl)),host(sK4_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f1465])).
% 21.68/13.31 fof(f1467,plain,(
% 21.68/13.31 leq(host(sK4_skl),host(sK8_skl))|~elec_2=elec_2|leq(host(sK12_skl),host(sK4_skl))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f930,f1466])).
% 21.68/13.31 fof(f1468,plain,(
% 21.68/13.31 leq(host(sK4_skl),host(sK8_skl))|leq(host(sK12_skl),host(sK4_skl))),
% 21.68/13.31 inference(trivial_equality_resolution,[status(thm)],[f1467])).
% 21.68/13.31 fof(f1578,plain,(
% 21.68/13.31 ![X0,X1]: (~setIn(X0,alive)|~host(sK4_skl)=host(X1)|~index(status,host(X0))=elec_2|~elec_2=elec_2|~elem(m_Ack(X0,X1),queue(host(X0))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f237,f475])).
% 21.68/13.31 fof(f1579,plain,(
% 21.68/13.31 ![X0,X1]: (~setIn(X0,alive)|~host(sK4_skl)=host(X1)|~index(status,host(X0))=elec_2|~elem(m_Ack(X0,X1),queue(host(X0))))),
% 21.68/13.31 inference(trivial_equality_resolution,[status(thm)],[f1578])).
% 21.68/13.31 fof(f1582,plain,(
% 21.68/13.31 ![X0]: (~setIn(sK10_skl,alive)|~host(sK4_skl)=host(X0)|~index(status,host(sK10_skl))=elec_2|~elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl))))),
% 21.68/13.31 inference(paramodulation,[status(thm)],[f242,f1579])).
% 21.68/13.31 fof(f1585,plain,(
% 21.68/13.31 ![X0]: (~setIn(sK10_skl,alive)|~host(sK4_skl)=host(X0)|~index(status,host(sK8_skl))=elec_2|~elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f1582])).
% 21.68/13.31 fof(f1586,plain,(
% 21.68/13.31 ![X0]: (~setIn(sK10_skl,alive)|~host(sK4_skl)=host(X0)|~elec_2=elec_2|~elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f854,f1585])).
% 21.68/13.31 fof(f1587,plain,(
% 21.68/13.31 ![X0]: (~setIn(sK10_skl,alive)|~host(sK4_skl)=host(X0)|~elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl))))),
% 21.68/13.31 inference(trivial_equality_resolution,[status(thm)],[f1586])).
% 21.68/13.31 fof(f1588,plain,(
% 21.68/13.31 ![X0]: (~host(sK4_skl)=host(X0)|~elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl))))),
% 21.68/13.31 inference(forward_subsumption_resolution,[status(thm)],[f1587,f244])).
% 21.68/13.31 fof(f1699,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK10_skl),host(X0))|~setIn(X0,alive)|~index(status,host(sK10_skl))=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),index(pendack,host(sK10_skl))))),
% 21.68/13.31 inference(resolution,[status(thm)],[f558,f244])).
% 21.68/13.31 fof(f1717,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK8_skl),host(X0))|~setIn(X0,alive)|~index(status,host(sK10_skl))=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),index(pendack,host(sK10_skl))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f1699])).
% 21.68/13.31 fof(f1718,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK8_skl),host(X0))|~setIn(X0,alive)|~index(status,host(sK8_skl))=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),index(pendack,host(sK10_skl))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f1717])).
% 21.68/13.31 fof(f1719,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK8_skl),host(X0))|~setIn(X0,alive)|~elec_2=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),index(pendack,host(sK10_skl))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f854,f1718])).
% 21.68/13.31 fof(f1720,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK8_skl),host(X0))|~setIn(X0,alive)|~elec_2=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),index(pendack,host(sK8_skl))))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f242,f1719])).
% 21.68/13.31 fof(f1721,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK8_skl),host(X0))|~setIn(X0,alive)|~elec_2=elec_2|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK12_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f930,f1720])).
% 21.68/13.31 fof(f1722,plain,(
% 21.68/13.31 ![X0]: (leq(host(sK8_skl),host(X0))|~setIn(X0,alive)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK12_skl)))),
% 21.68/13.31 inference(trivial_equality_resolution,[status(thm)],[f1721])).
% 21.68/13.31 fof(f2508,plain,(
% 21.68/13.31 ~host(sK5_skl)=host(sK4_skl)),
% 21.68/13.31 inference(resolution,[status(thm)],[f795,f216])).
% 21.68/13.31 fof(f2565,plain,(
% 21.68/13.31 ~nbr_proc=host(sK4_skl)),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f822,f2508])).
% 21.68/13.31 fof(f3346,plain,(
% 21.68/13.31 ![X0]: (~leq(X0,nbr_proc)|X0=host(sK11_skl)|leq(X0,host(sK12_skl)))),
% 21.68/13.31 inference(forward_demodulation,[status(thm)],[f978,f956])).
% 21.68/13.31 fof(f3347,plain,(
% 21.68/13.31 ![X0]: (~leq(X0,nbr_proc)|X0=nbr_proc|leq(X0,host(sK12_skl)))),
% 19.55/13.34 inference(forward_demodulation,[status(thm)],[f978,f3346])).
% 19.55/13.34 fof(f3350,plain,(
% 19.55/13.34 ![X0]: (host(X0)=nbr_proc|leq(host(X0),host(sK12_skl)))),
% 19.55/13.34 inference(resolution,[status(thm)],[f3347,f76])).
% 19.55/13.34 fof(f7320,plain,(
% 19.55/13.34 ~host(sK4_skl)=host(sK12_skl)),
% 19.55/13.34 inference(resolution,[status(thm)],[f1588,f853])).
% 19.55/13.34 fof(f7741,plain,(
% 19.55/13.34 leq(host(sK8_skl),host(sK4_skl))|~index(status,host(sK4_skl))=elec_2|leq(index(pendack,host(sK4_skl)),host(sK12_skl))),
% 19.55/13.34 inference(resolution,[status(thm)],[f1722,f235])).
% 19.55/13.34 fof(f7748,plain,(
% 19.55/13.34 leq(host(sK8_skl),host(sK4_skl))|~elec_2=elec_2|leq(index(pendack,host(sK4_skl)),host(sK12_skl))),
% 19.55/13.34 inference(forward_demodulation,[status(thm)],[f237,f7741])).
% 19.55/13.34 fof(f7749,plain,(
% 19.55/13.34 leq(host(sK8_skl),host(sK4_skl))|~elec_2=elec_2|leq(nbr_proc,host(sK12_skl))),
% 19.55/13.34 inference(forward_demodulation,[status(thm)],[f856,f7748])).
% 19.55/13.34 fof(f7750,plain,(
% 19.55/13.34 leq(host(sK8_skl),host(sK4_skl))|leq(nbr_proc,host(sK12_skl))),
% 19.55/13.34 inference(trivial_equality_resolution,[status(thm)],[f7749])).
% 19.55/13.34 fof(f7751,plain,(
% 19.55/13.34 leq(host(sK8_skl),host(sK4_skl))),
% 19.55/13.34 inference(forward_subsumption_resolution,[status(thm)],[f7750,f1084])).
% 19.55/13.34 fof(f7762,plain,(
% 19.55/13.34 ~leq(host(sK4_skl),host(sK8_skl))|host(sK4_skl)=host(sK8_skl)),
% 19.55/13.34 inference(resolution,[status(thm)],[f7751,f196])).
% 19.55/13.34 fof(f7764,plain,(
% 19.55/13.34 ~leq(host(sK4_skl),host(sK8_skl))),
% 19.55/13.34 inference(forward_subsumption_resolution,[status(thm)],[f7762,f430])).
% 19.55/13.34 fof(f7766,plain,(
% 19.55/13.34 leq(host(sK12_skl),host(sK4_skl))),
% 19.55/13.34 inference(backward_subsumption_resolution,[status(thm)],[f1468,f7764])).
% 19.55/13.34 fof(f7867,plain,(
% 19.55/13.34 ~leq(host(sK4_skl),host(sK12_skl))|host(sK4_skl)=host(sK12_skl)),
% 19.55/13.34 inference(resolution,[status(thm)],[f7766,f196])).
% 19.55/13.34 fof(f7870,plain,(
% 19.55/13.34 ~leq(host(sK4_skl),host(sK12_skl))),
% 19.55/13.34 inference(forward_subsumption_resolution,[status(thm)],[f7867,f7320])).
% 19.55/13.34 fof(f8063,plain,(
% 19.55/13.34 host(sK4_skl)=nbr_proc),
% 19.55/13.34 inference(resolution,[status(thm)],[f7870,f3350])).
% 19.55/13.34 fof(f8074,plain,(
% 19.55/13.34 $false),
% 19.55/13.34 inference(forward_subsumption_resolution,[status(thm)],[f8063,f2565])).
% 19.55/13.34 % SZS output end CNFRefutation for theBenchmark.p
% 19.55/13.36 % Elapsed time: 2.901100 seconds
% 19.55/13.36 % CPU time: 22.673983 seconds
% 19.55/13.36 % Total memory used: 216.491 MB
% 19.55/13.36 % Net memory used: 195.397 MB
%------------------------------------------------------------------------------