%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV475+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 : n020.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:55 PM UTC 2026
% Result : Theorem 33.46s 4.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV475+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.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % 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:54:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 33.46/4.68 % Refutation found
% 33.46/4.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 33.46/4.68 % SZS output start CNFRefutation for theBenchmark
% 33.46/4.68 fof(f3,axiom,(
% 33.46/4.68 (! [P] : leq(s(zero),host(P)) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f5,axiom,(
% 33.46/4.68 (! [P] : leq(host(P),nbr_proc) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f19,axiom,(
% 33.46/4.68 (! [X,Y] : m_Down(X) != m_Ldr(Y) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f48,axiom,(
% 33.46/4.68 (! [X,Y,Q] :( elem(X,snoc(Q,Y))<=> ( X = Y| elem(X,Q) ) ) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f59,axiom,(
% 33.46/4.68 (! [X] : ~ leq(s(X),X) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f62,axiom,(
% 33.46/4.68 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f63,axiom,(
% 33.46/4.68 (! [X,Y,Z] :( ( leq(X,Y)& leq(Y,Z) )=> leq(X,Z) ) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f65,axiom,(
% 33.46/4.68 (! [X,Y] :( leq(X,s(Y))<=> ( X = s(Y)| leq(X,Y) ) ) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f67,conjecture,(
% 33.46/4.68 (! [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] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [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] :( ( 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] :( ( setIn(Z,alive)& setIn(Pid0,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> Pid0 = Z ))& (! [Z,Pid20,Pid0] :( ( ~ leq(host(Pid20),host(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,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& elem(m_Down(Pid30),queue(host(Pid20))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& setIn(host(Pid30),index(down,host(Pid20))) ) ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& host(Pid20) = host(Z)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid20) )=> ~ ( setIn(Pid20,alive)& index(status,host(Pid20)) = norm& index(ldr,host(Pid20)) = host(Pid20) ) ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& host(Pid20) = host(Z)& index(status,host(Pid0)) = wait& host(index(elid,host(Pid0))) = host(Pid20) )=> ~ ( setIn(Pid20,alive)& index(status,host(Pid20)) = norm& index(ldr,host(Pid20)) = host(Pid20) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& setIn(Z,alive)& leq(host(Z),host(Pid0))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid30) = host(Pid0)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_1 )=> ~ elem(m_Ack(Z,Pid30),queue(host(Z))) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& setIn(Pid0,alive)& leq(nbr_proc,s(host(Pid0)))& elem(m_Down(Pid20),queue(host(Pid0)))& elem(m_Down(Pid30),queue(host(Pid0)))& host(Pid30) = s(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_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] :( ( setIn(host(Z),index(acks,host(X)))| host(Z) = host(Y) )=> (! [V0] :( host(X) = host(V0)=> (! [W0,X0,Y0] :( host(Z) = host(Y0)=> ( host(X) != host(Y0)=> ( ( (! [V1] :( ( ~ leq(host(Y0),V1)& leq(s(zero),V1) )=> ( setIn(V1,index(down,host(Y0)))| V1 = host(X0) ) ))& setIn(Y0,alive)& leq(nbr_proc,s(host(Y0)))& elem(m_Down(W0),snoc(queue(host(Y0)),m_Ldr(X)))& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))& host(W0) = s(host(Y0))& index(status,host(Y0)) = elec_1 )=> ~ ( setIn(V0,alive)& host(X) = host(V0) ) ) ) ) )) )) )) ) ) ) )),
% 33.46/4.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.46/4.68 fof(f68,negated_conjecture,(
% 33.46/4.68 ~((! [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] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [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] :( ( 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] :( ( setIn(Z,alive)& setIn(Pid0,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> Pid0 = Z ))& (! [Z,Pid20,Pid0] :( ( ~ leq(host(Pid20),host(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,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& elem(m_Down(Pid30),queue(host(Pid20))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& setIn(host(Pid30),index(down,host(Pid20))) ) ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& host(Pid20) = host(Z)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid20) )=> ~ ( setIn(Pid20,alive)& index(status,host(Pid20)) = norm& index(ldr,host(Pid20)) = host(Pid20) ) ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& host(Pid20) = host(Z)& index(status,host(Pid0)) = wait& host(index(elid,host(Pid0))) = host(Pid20) )=> ~ ( setIn(Pid20,alive)& index(status,host(Pid20)) = norm& index(ldr,host(Pid20)) = host(Pid20) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& setIn(Z,alive)& leq(host(Z),host(Pid0))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid30) = host(Pid0)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_1 )=> ~ elem(m_Ack(Z,Pid30),queue(host(Z))) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& setIn(Pid0,alive)& leq(nbr_proc,s(host(Pid0)))& elem(m_Down(Pid20),queue(host(Pid0)))& elem(m_Down(Pid30),queue(host(Pid0)))& host(Pid30) = s(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_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] :( ( setIn(host(Z),index(acks,host(X)))| host(Z) = host(Y) )=> (! [V0] :( host(X) = host(V0)=> (! [W0,X0,Y0] :( host(Z) = host(Y0)=> ( host(X) != host(Y0)=> ( ( (! [V1] :( ( ~ leq(host(Y0),V1)& leq(s(zero),V1) )=> ( setIn(V1,index(down,host(Y0)))| V1 = host(X0) ) ))& setIn(Y0,alive)& leq(nbr_proc,s(host(Y0)))& elem(m_Down(W0),snoc(queue(host(Y0)),m_Ldr(X)))& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))& host(W0) = s(host(Y0))& index(status,host(Y0)) = elec_1 )=> ~ ( setIn(V0,alive)& host(X) = host(V0) ) ) ) ) )) )) )) ) ) ) ))),
% 33.46/4.68 inference(negated_conjecture,[status(cth)],[f67])).
% 33.46/4.68 fof(f74,plain,(
% 33.46/4.68 ![X0]: (leq(s(zero),host(X0)))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f3])).
% 33.46/4.68 fof(f76,plain,(
% 33.46/4.68 ![X0]: (leq(host(X0),nbr_proc))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f5])).
% 33.46/4.68 fof(f90,plain,(
% 33.46/4.68 ![X0,X1]: (~m_Down(X0)=m_Ldr(X1))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f19])).
% 33.46/4.68 fof(f143,plain,(
% 33.46/4.68 ![X,Y,Q]: ((~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q)))&(elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 33.46/4.68 inference(NNF_transformation,[status(thm)],[f48])).
% 33.46/4.68 fof(f144,plain,(
% 33.46/4.68 (![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))))),
% 33.46/4.68 inference(miniscoping,[status(thm)],[f143])).
% 33.46/4.68 fof(f145,plain,(
% 33.46/4.68 ![X0,X1,X2]: (~elem(X0,snoc(X1,X2))|X0=X2|elem(X0,X1))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f144])).
% 33.46/4.68 fof(f191,plain,(
% 33.46/4.68 ![X0]: (~leq(s(X0),X0))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f59])).
% 33.46/4.68 fof(f194,plain,(
% 33.46/4.68 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 33.46/4.68 inference(NNF_transformation,[status(thm)],[f62])).
% 33.46/4.68 fof(f195,plain,(
% 33.46/4.68 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 33.46/4.68 inference(miniscoping,[status(thm)],[f194])).
% 33.46/4.68 fof(f196,plain,(
% 33.46/4.68 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f195])).
% 33.46/4.68 fof(f199,plain,(
% 33.46/4.68 ![X,Y,Z]: ((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))),
% 33.46/4.68 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 33.46/4.68 fof(f200,plain,(
% 33.46/4.68 ![X,Z]: ((![Y]: (~leq(X,Y)|~leq(Y,Z)))|leq(X,Z))),
% 33.46/4.68 inference(miniscoping,[status(thm)],[f199])).
% 33.46/4.68 fof(f201,plain,(
% 33.46/4.68 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f200])).
% 33.46/4.68 fof(f206,plain,(
% 33.46/4.68 ![X,Y]: ((~leq(X,s(Y))|(X=s(Y)|leq(X,Y)))&(leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 33.46/4.68 inference(NNF_transformation,[status(thm)],[f65])).
% 33.46/4.68 fof(f207,plain,(
% 33.46/4.68 (![X,Y]: (~leq(X,s(Y))|(X=s(Y)|leq(X,Y))))&(![X,Y]: (leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 33.46/4.68 inference(miniscoping,[status(thm)],[f206])).
% 33.46/4.68 fof(f208,plain,(
% 33.46/4.68 ![X0,X1]: (~leq(X0,s(X1))|X0=s(X1)|leq(X0,X1))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f207])).
% 33.46/4.68 fof(f212,plain,(
% 33.46/4.68 (?[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]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![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]: (((((~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]: ((((((~setIn(Z,alive)|~setIn(Pid0,alive))|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|Pid0=Z)))&(![Z,Pid20,Pid0]: ((((leq(host(Pid20),host(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,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~elem(m_Down(Pid30),queue(host(Pid20)))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~setIn(host(Pid30),index(down,host(Pid20)))))))&(![Z,Pid20,Pid0]: ((((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~elem(m_Down(Z),queue(host(Pid0))))|~host(Pid20)=host(Z))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid20))|((~setIn(Pid20,alive)|~index(status,host(Pid20))=norm)|~index(ldr,host(Pid20))=host(Pid20)))))&(![Z,Pid20,Pid0]: ((((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~elem(m_Down(Z),queue(host(Pid0))))|~host(Pid20)=host(Z))|~index(status,host(Pid0))=wait)|~host(index(elid,host(Pid0)))=host(Pid20))|((~setIn(Pid20,alive)|~index(status,host(Pid20))=norm)|~index(ldr,host(Pid20))=host(Pid20)))))&(![Z,Pid30,Pid20,Pid0]: ((((((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~setIn(Z,alive))|~leq(host(Z),host(Pid0)))|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid30)=host(Pid0))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_1)|~elem(m_Ack(Z,Pid30),queue(host(Z))))))&(![Z,Pid30,Pid20,Pid0]: ((((((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~setIn(Pid0,alive))|~leq(nbr_proc,s(host(Pid0))))|~elem(m_Down(Pid20),queue(host(Pid0))))|~elem(m_Down(Pid30),queue(host(Pid0))))|~host(Pid30)=s(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_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]: ((setIn(host(Z),index(acks,host(X)))|host(Z)=host(Y))&(?[V0]: (host(X)=host(V0)&(?[W0,X0,Y0]: (host(Z)=host(Y0)&(~host(X)=host(Y0)&((((((((![V1]: ((leq(host(Y0),V1)|~leq(s(zero),V1))|(setIn(V1,index(down,host(Y0)))|V1=host(X0))))&setIn(Y0,alive))&leq(nbr_proc,s(host(Y0))))&elem(m_Down(W0),snoc(queue(host(Y0)),m_Ldr(X))))&elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X))))&host(W0)=s(host(Y0)))&index(status,host(Y0))=elec_1)&(setIn(V0,alive)&host(X)=host(V0)))))))))))))))),
% 33.46/4.68 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 33.46/4.68 fof(f213,plain,(
% 33.46/4.68 ?[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]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![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,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]: ((((((~setIn(Z,alive)|~setIn(Pid0,alive))|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|Pid0=Z)))&(![Z]: ((![Pid20]: ((![Pid0]: ((leq(host(Pid20),host(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,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~elem(m_Down(Pid30),queue(host(Pid20)))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~setIn(host(Pid30),index(down,host(Pid20)))))))&(![Pid20]: ((![Pid0]: (((![Z]: (((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~elem(m_Down(Z),queue(host(Pid0))))|~host(Pid20)=host(Z)))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid20)))|((~setIn(Pid20,alive)|~index(status,host(Pid20))=norm)|~index(ldr,host(Pid20))=host(Pid20)))))&(![Pid20]: ((![Pid0]: (((![Z]: (((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~elem(m_Down(Z),queue(host(Pid0))))|~host(Pid20)=host(Z)))|~index(status,host(Pid0))=wait)|~host(index(elid,host(Pid0)))=host(Pid20)))|((~setIn(Pid20,alive)|~index(status,host(Pid20))=norm)|~index(ldr,host(Pid20))=host(Pid20)))))&(![Z,Pid30]: ((![Pid0]: ((((![Pid20]: ((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~setIn(Z,alive))|~leq(host(Z),host(Pid0)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid30)=host(Pid0))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_1))|~elem(m_Ack(Z,Pid30),queue(host(Z))))))&((![Pid0]: ((![Pid30]: (((![Pid20]: ((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~setIn(Pid0,alive))|~leq(nbr_proc,s(host(Pid0))))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~elem(m_Down(Pid30),queue(host(Pid0))))|~host(Pid30)=s(host(Pid0))))|~index(status,host(Pid0))=elec_1))|(![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)))&(?[Z]: ((setIn(host(Z),index(acks,host(X)))|host(Z)=host(Y))&(?[V0]: (host(X)=host(V0)&(?[Y0]: (host(Z)=host(Y0)&(~host(X)=host(Y0)&(((?[W0]: ((?[X0]: (((((![V1]: ((leq(host(Y0),V1)|~leq(s(zero),V1))|(setIn(V1,index(down,host(Y0)))|V1=host(X0))))&setIn(Y0,alive))&leq(nbr_proc,s(host(Y0))))&elem(m_Down(W0),snoc(queue(host(Y0)),m_Ldr(X))))&elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))))&host(W0)=s(host(Y0))))&index(status,host(Y0))=elec_1)&(setIn(V0,alive)&host(X)=host(V0))))))))))))))),
% 33.46/4.68 inference(miniscoping,[status(thm)],[f212])).
% 33.46/4.68 fof(f214,plain,(
% 33.46/4.68 ((((((((((((((((((![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]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![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,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]: ((((((~setIn(Z,alive)|~setIn(Pid0,alive))|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|Pid0=Z)))&(![Z]: ((![Pid20]: ((![Pid0]: ((leq(host(Pid20),host(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,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~elem(m_Down(Pid30),queue(host(Pid20)))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~setIn(host(Pid30),index(down,host(Pid20)))))))&(![Pid20]: ((![Pid0]: (((![Z]: (((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~elem(m_Down(Z),queue(host(Pid0))))|~host(Pid20)=host(Z)))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid20)))|((~setIn(Pid20,alive)|~index(status,host(Pid20))=norm)|~index(ldr,host(Pid20))=host(Pid20)))))&(![Pid20]: ((![Pid0]: (((![Z]: (((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~elem(m_Down(Z),queue(host(Pid0))))|~host(Pid20)=host(Z)))|~index(status,host(Pid0))=wait)|~host(index(elid,host(Pid0)))=host(Pid20)))|((~setIn(Pid20,alive)|~index(status,host(Pid20))=norm)|~index(ldr,host(Pid20))=host(Pid20)))))&(![Z,Pid30]: ((![Pid0]: ((((![Pid20]: (((((~leq(host(Pid0),sK7_skl(Pid20,Pid0,Pid30,Z))&leq(s(zero),sK7_skl(Pid20,Pid0,Pid30,Z)))&(~setIn(sK7_skl(Pid20,Pid0,Pid30,Z),index(down,host(Pid0)))&~sK7_skl(Pid20,Pid0,Pid30,Z)=host(Pid20)))|~setIn(Z,alive))|~leq(host(Z),host(Pid0)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid30)=host(Pid0))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_1))|~elem(m_Ack(Z,Pid30),queue(host(Z))))))&((![Pid0]: ((![Pid30]: (((![Pid20]: (((((~leq(host(Pid0),sK8_skl(Pid20,Pid30,Pid0))&leq(s(zero),sK8_skl(Pid20,Pid30,Pid0)))&(~setIn(sK8_skl(Pid20,Pid30,Pid0),index(down,host(Pid0)))&~sK8_skl(Pid20,Pid30,Pid0)=host(Pid20)))|~setIn(Pid0,alive))|~leq(nbr_proc,s(host(Pid0))))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~elem(m_Down(Pid30),queue(host(Pid0))))|~host(Pid30)=s(host(Pid0))))|~index(status,host(Pid0))=elec_1))|(![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),sK9_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)))&((setIn(host(sK10_skl),index(acks,host(sK5_skl)))|host(sK10_skl)=host(sK6_skl))&(host(sK5_skl)=host(sK11_skl)&(host(sK10_skl)=host(sK12_skl)&(~host(sK5_skl)=host(sK12_skl)&((((((((![V1]: ((leq(host(sK12_skl),V1)|~leq(s(zero),V1))|(setIn(V1,index(down,host(sK12_skl)))|V1=host(sK14_skl))))&setIn(sK12_skl,alive))&leq(nbr_proc,s(host(sK12_skl))))&elem(m_Down(sK13_skl),snoc(queue(host(sK12_skl)),m_Ldr(sK5_skl))))&elem(m_Down(sK14_skl),snoc(queue(host(sK12_skl)),m_Ldr(sK5_skl))))&host(sK13_skl)=s(host(sK12_skl)))&index(status,host(sK12_skl))=elec_1)&(setIn(sK11_skl,alive)&host(sK5_skl)=host(sK11_skl)))))))))))),
% 33.46/4.68 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,sK13_skl,sK14_skl]),skolemize(W,sK4_skl),skolemize(X,sK5_skl),skolemize(Y,sK6_skl),skolemize(V0,sK7_skl(Pid20,Pid0,Pid30,Z)),skolemize(V0,sK8_skl(Pid20,Pid30,Pid0)),skolemize(V,sK9_skl),skolemize(Z,sK10_skl),skolemize(V0,sK11_skl),skolemize(Y0,sK12_skl),skolemize(W0,sK13_skl),skolemize(X0,sK14_skl)],[f213])).
% 33.46/4.68 fof(f219,plain,(
% 33.46/4.68 ![X0]: (~index(status,host(X0))=elec_2|~setIn(X0,alive)|index(elid,host(X0))=X0)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f220,plain,(
% 33.46/4.68 ![X0,X1]: (~setIn(X0,alive)|~setIn(X1,alive)|~setIn(host(X1),index(down,host(X0)))|~index(status,host(X1))=elec_2|leq(index(pendack,host(X1)),host(X0)))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f222,plain,(
% 33.46/4.68 ![X0,X1,X2]: (~setIn(X0,alive)|~setIn(X1,alive)|~elem(m_Down(X2),queue(host(X0)))|~host(X1)=host(X2)|~index(status,host(X1))=elec_2|leq(index(pendack,host(X1)),host(X0)))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f239,plain,(
% 33.46/4.68 setIn(sK5_skl,alive)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f240,plain,(
% 33.46/4.68 index(elid,host(sK5_skl))=sK4_skl),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f241,plain,(
% 33.46/4.68 index(status,host(sK5_skl))=elec_2),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f242,plain,(
% 33.46/4.68 host(sK6_skl)=index(pendack,host(sK5_skl))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f243,plain,(
% 33.46/4.68 leq(nbr_proc,index(pendack,host(sK5_skl)))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f245,plain,(
% 33.46/4.68 host(sK5_skl)=host(sK11_skl)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f246,plain,(
% 33.46/4.68 host(sK10_skl)=host(sK12_skl)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f247,plain,(
% 33.46/4.68 ~host(sK5_skl)=host(sK12_skl)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f248,plain,(
% 33.46/4.68 ![X0]: (leq(host(sK12_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK12_skl)))|X0=host(sK14_skl))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f249,plain,(
% 33.46/4.68 setIn(sK12_skl,alive)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f250,plain,(
% 33.46/4.68 leq(nbr_proc,s(host(sK12_skl)))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f251,plain,(
% 33.46/4.68 elem(m_Down(sK13_skl),snoc(queue(host(sK12_skl)),m_Ldr(sK5_skl)))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f252,plain,(
% 33.46/4.68 elem(m_Down(sK14_skl),snoc(queue(host(sK12_skl)),m_Ldr(sK5_skl)))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f253,plain,(
% 33.46/4.68 host(sK13_skl)=s(host(sK12_skl))),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f255,plain,(
% 33.46/4.68 setIn(sK11_skl,alive)),
% 33.46/4.68 inference(cnf_transformation,[status(thm)],[f214])).
% 33.46/4.68 fof(f276,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(sK11_skl,alive)|~setIn(host(sK11_skl),index(down,host(X0)))|~index(status,host(sK11_skl))=elec_2|leq(index(pendack,host(sK5_skl)),host(X0)))),
% 33.46/4.68 inference(paramodulation,[status(thm)],[f245,f220])).
% 33.46/4.68 fof(f289,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(sK11_skl,alive)|~setIn(host(sK5_skl),index(down,host(X0)))|~index(status,host(sK11_skl))=elec_2|leq(index(pendack,host(sK5_skl)),host(X0)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f245,f276])).
% 33.46/4.68 fof(f290,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(sK11_skl,alive)|~setIn(host(sK5_skl),index(down,host(X0)))|~index(status,host(sK5_skl))=elec_2|leq(index(pendack,host(sK5_skl)),host(X0)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f245,f289])).
% 33.46/4.68 fof(f291,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(host(sK5_skl),index(down,host(X0)))|~index(status,host(sK5_skl))=elec_2|leq(index(pendack,host(sK5_skl)),host(X0)))),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f290,f255])).
% 33.46/4.68 fof(f343,plain,(
% 33.46/4.68 ![X0,X1]: (~setIn(sK12_skl,alive)|~setIn(X0,alive)|~elem(m_Down(X1),queue(host(sK10_skl)))|~host(X0)=host(X1)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK12_skl)))),
% 33.46/4.68 inference(paramodulation,[status(thm)],[f246,f222])).
% 33.46/4.68 fof(f358,plain,(
% 33.46/4.68 ![X0,X1]: (~setIn(sK12_skl,alive)|~setIn(X0,alive)|~elem(m_Down(X1),queue(host(sK10_skl)))|~host(X0)=host(X1)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK10_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f343])).
% 33.46/4.68 fof(f359,plain,(
% 33.46/4.68 ![X0,X1]: (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(sK10_skl)))|~host(X0)=host(X1)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK10_skl)))),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f358,f249])).
% 33.46/4.68 fof(f418,plain,(
% 33.46/4.68 ~host(sK5_skl)=host(sK10_skl)),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f247])).
% 33.46/4.68 fof(f439,plain,(
% 33.46/4.68 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|~leq(X2,X0)|X2=X0)),
% 33.46/4.68 inference(resolution,[status(thm)],[f201,f196])).
% 33.46/4.68 fof(f559,plain,(
% 33.46/4.68 ~setIn(sK5_skl,alive)|index(elid,host(sK5_skl))=sK5_skl),
% 33.46/4.68 inference(resolution,[status(thm)],[f241,f219])).
% 33.46/4.68 fof(f562,plain,(
% 33.46/4.68 ~setIn(sK5_skl,alive)|sK4_skl=sK5_skl),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f240,f559])).
% 33.46/4.68 fof(f563,plain,(
% 33.46/4.68 sK4_skl=sK5_skl),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f562,f239])).
% 33.46/4.68 fof(f583,plain,(
% 33.46/4.68 index(status,host(sK4_skl))=elec_2),
% 33.46/4.68 inference(backward_demodulation,[status(thm)],[f563,f241])).
% 33.46/4.68 fof(f585,plain,(
% 33.46/4.68 ~host(sK4_skl)=host(sK10_skl)),
% 33.46/4.68 inference(backward_demodulation,[status(thm)],[f563,f418])).
% 33.46/4.68 fof(f587,plain,(
% 33.46/4.68 setIn(sK4_skl,alive)),
% 33.46/4.68 inference(backward_demodulation,[status(thm)],[f563,f239])).
% 33.46/4.68 fof(f611,plain,(
% 33.46/4.68 host(sK6_skl)=index(pendack,host(sK4_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f563,f242])).
% 33.46/4.68 fof(f694,plain,(
% 33.46/4.68 leq(nbr_proc,index(pendack,host(sK4_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f563,f243])).
% 33.46/4.68 fof(f695,plain,(
% 33.46/4.68 leq(nbr_proc,host(sK6_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f611,f694])).
% 33.46/4.68 fof(f696,plain,(
% 33.46/4.68 ~leq(host(sK6_skl),nbr_proc)|host(sK6_skl)=nbr_proc),
% 33.46/4.68 inference(resolution,[status(thm)],[f695,f196])).
% 33.46/4.68 fof(f697,plain,(
% 33.46/4.68 host(sK6_skl)=nbr_proc),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f696,f76])).
% 33.46/4.68 fof(f699,plain,(
% 33.46/4.68 ![X0]: (leq(host(sK10_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK12_skl)))|X0=host(sK14_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f248])).
% 33.46/4.68 fof(f700,plain,(
% 33.46/4.68 ![X0]: (leq(host(sK10_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK10_skl)))|X0=host(sK14_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f699])).
% 33.46/4.68 fof(f703,plain,(
% 33.46/4.68 leq(nbr_proc,s(host(sK10_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f250])).
% 33.46/4.68 fof(f706,plain,(
% 33.46/4.68 elem(m_Down(sK13_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK5_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f251])).
% 33.46/4.68 fof(f707,plain,(
% 33.46/4.68 elem(m_Down(sK13_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f563,f706])).
% 33.46/4.68 fof(f708,plain,(
% 33.46/4.68 m_Down(sK13_skl)=m_Ldr(sK4_skl)|elem(m_Down(sK13_skl),queue(host(sK10_skl)))),
% 33.46/4.68 inference(resolution,[status(thm)],[f707,f145])).
% 33.46/4.68 fof(f709,plain,(
% 33.46/4.68 elem(m_Down(sK13_skl),queue(host(sK10_skl)))),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f708,f90])).
% 33.46/4.68 fof(f710,plain,(
% 33.46/4.68 elem(m_Down(sK14_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK5_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f252])).
% 33.46/4.68 fof(f711,plain,(
% 33.46/4.68 elem(m_Down(sK14_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f563,f710])).
% 33.46/4.68 fof(f712,plain,(
% 33.46/4.68 m_Down(sK14_skl)=m_Ldr(sK4_skl)|elem(m_Down(sK14_skl),queue(host(sK10_skl)))),
% 33.46/4.68 inference(resolution,[status(thm)],[f711,f145])).
% 33.46/4.68 fof(f713,plain,(
% 33.46/4.68 elem(m_Down(sK14_skl),queue(host(sK10_skl)))),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f712,f90])).
% 33.46/4.68 fof(f716,plain,(
% 33.46/4.68 nbr_proc=index(pendack,host(sK4_skl))),
% 33.46/4.68 inference(backward_demodulation,[status(thm)],[f697,f611])).
% 33.46/4.68 fof(f789,plain,(
% 33.46/4.68 leq(nbr_proc,host(sK13_skl))),
% 33.46/4.68 inference(backward_demodulation,[status(thm)],[f790,f703])).
% 33.46/4.68 fof(f790,plain,(
% 33.46/4.68 host(sK13_skl)=s(host(sK10_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f253])).
% 33.46/4.68 fof(f795,plain,(
% 33.46/4.68 ![X0]: (~leq(X0,host(sK13_skl))|X0=s(host(sK10_skl))|leq(X0,host(sK10_skl)))),
% 33.46/4.68 inference(paramodulation,[status(thm)],[f790,f208])).
% 33.46/4.68 fof(f803,plain,(
% 33.46/4.68 ![X0]: (~leq(X0,host(sK13_skl))|X0=host(sK13_skl)|leq(X0,host(sK10_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f790,f795])).
% 33.46/4.68 fof(f809,plain,(
% 33.46/4.68 ~leq(host(sK13_skl),nbr_proc)|host(sK13_skl)=nbr_proc),
% 33.46/4.68 inference(resolution,[status(thm)],[f789,f196])).
% 33.46/4.68 fof(f810,plain,(
% 33.46/4.68 host(sK13_skl)=nbr_proc),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f809,f76])).
% 33.46/4.68 fof(f822,plain,(
% 33.46/4.68 nbr_proc=s(host(sK10_skl))),
% 33.46/4.68 inference(backward_demodulation,[status(thm)],[f810,f790])).
% 33.46/4.68 fof(f907,plain,(
% 33.46/4.68 ~leq(nbr_proc,host(sK10_skl))),
% 33.46/4.68 inference(paramodulation,[status(thm)],[f822,f191])).
% 33.46/4.68 fof(f953,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(host(sK4_skl),index(down,host(X0)))|~index(status,host(sK5_skl))=elec_2|leq(index(pendack,host(sK5_skl)),host(X0)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f563,f291])).
% 33.46/4.68 fof(f954,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(host(sK4_skl),index(down,host(X0)))|~index(status,host(sK4_skl))=elec_2|leq(index(pendack,host(sK5_skl)),host(X0)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f563,f953])).
% 33.46/4.68 fof(f955,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(host(sK4_skl),index(down,host(X0)))|~elec_2=elec_2|leq(index(pendack,host(sK5_skl)),host(X0)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f583,f954])).
% 33.46/4.68 fof(f956,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(host(sK4_skl),index(down,host(X0)))|~elec_2=elec_2|leq(index(pendack,host(sK4_skl)),host(X0)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f563,f955])).
% 33.46/4.68 fof(f957,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(host(sK4_skl),index(down,host(X0)))|~elec_2=elec_2|leq(nbr_proc,host(X0)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f716,f956])).
% 33.46/4.68 fof(f958,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~setIn(host(sK4_skl),index(down,host(X0)))|leq(nbr_proc,host(X0)))),
% 33.46/4.68 inference(trivial_equality_resolution,[status(thm)],[f957])).
% 33.46/4.68 fof(f960,plain,(
% 33.46/4.68 ~setIn(host(sK4_skl),index(down,host(sK12_skl)))|leq(nbr_proc,host(sK12_skl))),
% 33.46/4.68 inference(resolution,[status(thm)],[f958,f249])).
% 33.46/4.68 fof(f961,plain,(
% 33.46/4.68 ~setIn(host(sK4_skl),index(down,host(sK10_skl)))|leq(nbr_proc,host(sK12_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f960])).
% 33.46/4.68 fof(f962,plain,(
% 33.46/4.68 ~setIn(host(sK4_skl),index(down,host(sK10_skl)))|leq(nbr_proc,host(sK10_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f246,f961])).
% 33.46/4.68 fof(f1412,plain,(
% 33.46/4.68 ![X0,X1,X2,X3]: (~leq(X0,X1)|~leq(X2,X0)|X2=X0|~leq(X1,X3)|~leq(X3,X2))),
% 33.46/4.68 inference(resolution,[status(thm)],[f439,f201])).
% 33.46/4.68 fof(f1938,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~host(X0)=host(sK13_skl)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK10_skl)))),
% 33.46/4.68 inference(resolution,[status(thm)],[f709,f359])).
% 33.46/4.68 fof(f1960,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~host(X0)=nbr_proc|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK10_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f810,f1938])).
% 33.46/4.68 fof(f2045,plain,(
% 33.46/4.68 ![X0]: (~setIn(X0,alive)|~host(X0)=host(sK14_skl)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK10_skl)))),
% 33.46/4.68 inference(resolution,[status(thm)],[f713,f359])).
% 33.46/4.68 fof(f2127,plain,(
% 33.46/4.68 ![X0]: (~leq(X0,nbr_proc)|X0=host(sK13_skl)|leq(X0,host(sK10_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f810,f803])).
% 33.46/4.68 fof(f2128,plain,(
% 33.46/4.68 ![X0]: (~leq(X0,nbr_proc)|X0=nbr_proc|leq(X0,host(sK10_skl)))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f810,f2127])).
% 33.46/4.68 fof(f2131,plain,(
% 33.46/4.68 ![X0]: (host(X0)=nbr_proc|leq(host(X0),host(sK10_skl)))),
% 33.46/4.68 inference(resolution,[status(thm)],[f2128,f76])).
% 33.46/4.68 fof(f2486,plain,(
% 33.46/4.68 ~setIn(host(sK4_skl),index(down,host(sK10_skl)))),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f962,f907])).
% 33.46/4.68 fof(f2487,plain,(
% 33.46/4.68 leq(host(sK10_skl),host(sK4_skl))|~leq(s(zero),host(sK4_skl))|host(sK4_skl)=host(sK14_skl)),
% 33.46/4.68 inference(resolution,[status(thm)],[f2486,f700])).
% 33.46/4.68 fof(f2488,plain,(
% 33.46/4.68 leq(host(sK10_skl),host(sK4_skl))|host(sK4_skl)=host(sK14_skl)),
% 33.46/4.68 inference(forward_subsumption_resolution,[status(thm)],[f2487,f74])).
% 33.46/4.68 fof(f10997,plain,(
% 33.46/4.68 ~host(sK4_skl)=nbr_proc|~index(status,host(sK4_skl))=elec_2|leq(index(pendack,host(sK4_skl)),host(sK10_skl))),
% 33.46/4.68 inference(resolution,[status(thm)],[f1960,f587])).
% 33.46/4.68 fof(f10999,plain,(
% 33.46/4.68 ~host(sK4_skl)=nbr_proc|~elec_2=elec_2|leq(index(pendack,host(sK4_skl)),host(sK10_skl))),
% 33.46/4.68 inference(forward_demodulation,[status(thm)],[f583,f10997])).
% 33.46/4.68 fof(f11000,plain,(
% 33.46/4.68 ~host(sK4_skl)=nbr_proc|~elec_2=elec_2|leq(nbr_proc,host(sK10_skl))),
% 33.46/4.70 inference(forward_demodulation,[status(thm)],[f716,f10999])).
% 33.46/4.70 fof(f11001,plain,(
% 33.46/4.70 ~host(sK4_skl)=nbr_proc|leq(nbr_proc,host(sK10_skl))),
% 33.46/4.70 inference(trivial_equality_resolution,[status(thm)],[f11000])).
% 33.46/4.70 fof(f11002,plain,(
% 33.46/4.70 ~host(sK4_skl)=nbr_proc),
% 33.46/4.70 inference(forward_subsumption_resolution,[status(thm)],[f11001,f907])).
% 33.46/4.70 fof(f11202,plain,(
% 33.46/4.70 ~host(sK4_skl)=host(sK14_skl)|~index(status,host(sK4_skl))=elec_2|leq(index(pendack,host(sK4_skl)),host(sK10_skl))),
% 33.46/4.70 inference(resolution,[status(thm)],[f2045,f587])).
% 33.46/4.70 fof(f11204,plain,(
% 33.46/4.70 ~host(sK4_skl)=host(sK14_skl)|~elec_2=elec_2|leq(index(pendack,host(sK4_skl)),host(sK10_skl))),
% 33.46/4.70 inference(forward_demodulation,[status(thm)],[f583,f11202])).
% 33.46/4.70 fof(f11205,plain,(
% 33.46/4.70 ~host(sK4_skl)=host(sK14_skl)|~elec_2=elec_2|leq(nbr_proc,host(sK10_skl))),
% 33.46/4.70 inference(forward_demodulation,[status(thm)],[f716,f11204])).
% 33.46/4.70 fof(f11206,plain,(
% 33.46/4.70 ~host(sK4_skl)=host(sK14_skl)|leq(nbr_proc,host(sK10_skl))),
% 33.46/4.70 inference(trivial_equality_resolution,[status(thm)],[f11205])).
% 33.46/4.70 fof(f11207,plain,(
% 33.46/4.70 ~host(sK4_skl)=host(sK14_skl)),
% 33.46/4.70 inference(forward_subsumption_resolution,[status(thm)],[f11206,f907])).
% 33.46/4.70 fof(f13768,plain,(
% 33.46/4.70 leq(host(sK10_skl),host(sK4_skl))),
% 33.46/4.70 inference(forward_subsumption_resolution,[status(thm)],[f2488,f11207])).
% 33.46/4.70 fof(f13787,plain,(
% 33.46/4.70 ~leq(host(sK4_skl),host(sK10_skl))|host(sK10_skl)=host(sK4_skl)|~leq(host(sK4_skl),host(sK10_skl))),
% 33.46/4.70 inference(resolution,[status(thm)],[f13768,f1412])).
% 33.46/4.70 fof(f13795,plain,(
% 33.46/4.70 ~leq(host(sK4_skl),host(sK10_skl))|host(sK10_skl)=host(sK4_skl)),
% 33.46/4.70 inference(duplicate_literals_removal,[status(thm)],[f13787])).
% 33.46/4.70 fof(f13796,plain,(
% 33.46/4.70 ~leq(host(sK4_skl),host(sK10_skl))),
% 33.46/4.70 inference(forward_subsumption_resolution,[status(thm)],[f13795,f585])).
% 33.46/4.70 fof(f13849,plain,(
% 33.46/4.70 host(sK4_skl)=nbr_proc),
% 33.46/4.70 inference(resolution,[status(thm)],[f13796,f2131])).
% 33.46/4.70 fof(f13863,plain,(
% 33.46/4.70 $false),
% 33.46/4.70 inference(forward_subsumption_resolution,[status(thm)],[f13849,f11002])).
% 33.46/4.70 % SZS output end CNFRefutation for theBenchmark.p
% 33.46/4.73 % Elapsed time: 4.351862 seconds
% 33.46/4.73 % CPU time: 34.112831 seconds
% 33.46/4.73 % Total memory used: 306.832 MB
% 33.46/4.73 % Net memory used: 267.215 MB
%------------------------------------------------------------------------------