%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV460+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 : n026.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:53 PM UTC 2026
% Result : Theorem 3.73s 1.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV460+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 : n026.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:55:22 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 3.73/1.01 % Refutation found
% 3.73/1.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.73/1.01 % SZS output start CNFRefutation for theBenchmark
% 3.73/1.01 fof(f3,axiom,(
% 3.73/1.01 (! [P] : leq(s(zero),host(P)) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f4,axiom,(
% 3.73/1.01 leq(s(zero),nbr_proc) ),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f47,axiom,(
% 3.73/1.01 (! [X,Y,Q] :( elem(X,cons(Y,Q))<=> ( X = Y| elem(X,Q) ) ) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f59,axiom,(
% 3.73/1.01 (! [X] : ~ leq(s(X),X) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f61,axiom,(
% 3.73/1.01 (! [X,Y] :( leq(X,Y)| leq(Y,X) ) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f62,axiom,(
% 3.73/1.01 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f63,axiom,(
% 3.73/1.01 (! [X,Y,Z] :( ( leq(X,Y)& leq(Y,Z) )=> leq(X,Z) ) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f65,axiom,(
% 3.73/1.01 (! [X,Y] :( leq(X,s(Y))<=> ( X = s(Y)| leq(X,Y) ) ) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f67,conjecture,(
% 3.73/1.01 (! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Halt(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z] :( index(status,host(Z)) = elec_2=> ~ leq(index(pendack,host(Z)),host(Z)) ))& (! [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)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid0),queue(host(Z))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& setIn(host(Pid0),index(down,host(Z)))& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( ~ leq(host(Pid0),host(Z))& setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Down(Pid20),queue(host(Z))) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Z)))& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,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))) ))& queue(host(X)) = cons(m_Down(Y),V) )=> ( setIn(X,alive)=> ( ~ leq(host(X),host(Y))=> ( ~ ( ( index(ldr,host(X)) = host(Y)& index(status,host(X)) = norm )| ( index(status,host(X)) = wait& host(Y) = host(index(elid,host(X))) ) )=> ( ( (! [Z] :( ( ~ leq(host(X),Z)& leq(s(zero),Z) )=> ( setIn(Z,index(down,host(X)))| Z = host(Y) ) ))& index(status,host(X)) = elec_1 )=> ( ~ leq(nbr_proc,host(X))=> (! [Z] :( host(X) = host(Z)=> (! [W0] :( host(X) != host(W0)=> ( ( ~ leq(host(Z),host(W0))& setIn(Z,alive)& setIn(W0,alive)& index(status,host(W0)) = elec_2 )=> ~ leq(s(host(X)),index(pendack,host(W0))) ) ) )) )) ) ) ) ) ) )),
% 3.73/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.73/1.01 fof(f68,negated_conjecture,(
% 3.73/1.01 ~((! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Halt(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z] :( index(status,host(Z)) = elec_2=> ~ leq(index(pendack,host(Z)),host(Z)) ))& (! [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)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid0),queue(host(Z))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& setIn(host(Pid0),index(down,host(Z)))& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( ~ leq(host(Pid0),host(Z))& setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Down(Pid20),queue(host(Z))) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Z)))& host(Pid0) = host(Pid20)& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,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))) ))& queue(host(X)) = cons(m_Down(Y),V) )=> ( setIn(X,alive)=> ( ~ leq(host(X),host(Y))=> ( ~ ( ( index(ldr,host(X)) = host(Y)& index(status,host(X)) = norm )| ( index(status,host(X)) = wait& host(Y) = host(index(elid,host(X))) ) )=> ( ( (! [Z] :( ( ~ leq(host(X),Z)& leq(s(zero),Z) )=> ( setIn(Z,index(down,host(X)))| Z = host(Y) ) ))& index(status,host(X)) = elec_1 )=> ( ~ leq(nbr_proc,host(X))=> (! [Z] :( host(X) = host(Z)=> (! [W0] :( host(X) != host(W0)=> ( ( ~ leq(host(Z),host(W0))& setIn(Z,alive)& setIn(W0,alive)& index(status,host(W0)) = elec_2 )=> ~ leq(s(host(X)),index(pendack,host(W0))) ) ) )) )) ) ) ) ) ) ))),
% 3.73/1.01 inference(negated_conjecture,[status(cth)],[f67])).
% 3.73/1.01 fof(f74,plain,(
% 3.73/1.01 ![X0]: (leq(s(zero),host(X0)))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f3])).
% 3.73/1.01 fof(f75,plain,(
% 3.73/1.01 leq(s(zero),nbr_proc)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f4])).
% 3.73/1.01 fof(f138,plain,(
% 3.73/1.01 ![X,Y,Q]: ((~elem(X,cons(Y,Q))|(X=Y|elem(X,Q)))&(elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 3.73/1.01 inference(NNF_transformation,[status(thm)],[f47])).
% 3.73/1.01 fof(f139,plain,(
% 3.73/1.01 (![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))))),
% 3.73/1.01 inference(miniscoping,[status(thm)],[f138])).
% 3.73/1.01 fof(f141,plain,(
% 3.73/1.01 ![X0,X1,X2]: (elem(X0,cons(X1,X2))|~X0=X1)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f139])).
% 3.73/1.01 fof(f191,plain,(
% 3.73/1.01 ![X0]: (~leq(s(X0),X0))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f59])).
% 3.73/1.01 fof(f193,plain,(
% 3.73/1.01 ![X0,X1]: (leq(X0,X1)|leq(X1,X0))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f61])).
% 3.73/1.01 fof(f194,plain,(
% 3.73/1.01 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 3.73/1.01 inference(NNF_transformation,[status(thm)],[f62])).
% 3.73/1.01 fof(f195,plain,(
% 3.73/1.01 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 3.73/1.01 inference(miniscoping,[status(thm)],[f194])).
% 3.73/1.01 fof(f196,plain,(
% 3.73/1.01 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f195])).
% 3.73/1.01 fof(f199,plain,(
% 3.73/1.01 ![X,Y,Z]: ((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))),
% 3.73/1.01 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 3.73/1.01 fof(f200,plain,(
% 3.73/1.01 ![X,Z]: ((![Y]: (~leq(X,Y)|~leq(Y,Z)))|leq(X,Z))),
% 3.73/1.01 inference(miniscoping,[status(thm)],[f199])).
% 3.73/1.01 fof(f201,plain,(
% 3.73/1.01 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f200])).
% 3.73/1.01 fof(f206,plain,(
% 3.73/1.01 ![X,Y]: ((~leq(X,s(Y))|(X=s(Y)|leq(X,Y)))&(leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 3.73/1.01 inference(NNF_transformation,[status(thm)],[f65])).
% 3.73/1.01 fof(f207,plain,(
% 3.73/1.01 (![X,Y]: (~leq(X,s(Y))|(X=s(Y)|leq(X,Y))))&(![X,Y]: (leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 3.73/1.01 inference(miniscoping,[status(thm)],[f206])).
% 3.73/1.01 fof(f210,plain,(
% 3.73/1.01 ![X0,X1]: (leq(X0,s(X1))|~leq(X0,X1))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f207])).
% 3.73/1.01 fof(f212,plain,(
% 3.73/1.01 (?[V,W,X,Y]: ((((((((((((((![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z]: (~index(status,host(Z))=elec_2|~leq(index(pendack,host(Z)),host(Z)))))&(![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)|~index(status,host(Pid0))=elec_2)|~elem(m_Ack(Z,Pid0),queue(host(Z))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~setIn(host(Pid0),index(down,host(Z))))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20,Pid0]: (((((leq(host(Pid0),host(Z))|~setIn(Z,alive))|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2)|~elem(m_Down(Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20,Pid0]: (((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid20,Pid0]: (((((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Down(Pid20),queue(host(Z))))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,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))))))&queue(host(X))=cons(m_Down(Y),V))&(setIn(X,alive)&(~leq(host(X),host(Y))&(((~index(ldr,host(X))=host(Y)|~index(status,host(X))=norm)&(~index(status,host(X))=wait|~host(Y)=host(index(elid,host(X)))))&(((![Z]: ((leq(host(X),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(X)))|Z=host(Y))))&index(status,host(X))=elec_1)&(~leq(nbr_proc,host(X))&(?[Z]: (host(X)=host(Z)&(?[W0]: (~host(X)=host(W0)&((((~leq(host(Z),host(W0))&setIn(Z,alive))&setIn(W0,alive))&index(status,host(W0))=elec_2)&leq(s(host(X)),index(pendack,host(W0)))))))))))))))),
% 3.73/1.01 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 3.73/1.01 fof(f213,plain,(
% 3.73/1.01 ?[X,Y]: ((((((((((((((![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z]: (~index(status,host(Z))=elec_2|~leq(index(pendack,host(Z)),host(Z)))))&(![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)))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_2)|(![Z]: ~elem(m_Ack(Z,Pid0),queue(host(Z)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~setIn(host(Pid0),index(down,host(Z))))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20]: ((![Pid0]: ((((leq(host(Pid0),host(Z))|~setIn(Z,alive))|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2))|~elem(m_Down(Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20]: ((![Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid0]: (((![Pid20]: (((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Down(Pid20),queue(host(Z))))|~host(Pid0)=host(Pid20)))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![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))))))&(?[V]: queue(host(X))=cons(m_Down(Y),V)))&(setIn(X,alive)&(~leq(host(X),host(Y))&(((~index(ldr,host(X))=host(Y)|~index(status,host(X))=norm)&(~index(status,host(X))=wait|~host(Y)=host(index(elid,host(X)))))&(((![Z]: ((leq(host(X),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(X)))|Z=host(Y))))&index(status,host(X))=elec_1)&(~leq(nbr_proc,host(X))&(?[Z]: (host(X)=host(Z)&(?[W0]: (~host(X)=host(W0)&((((~leq(host(Z),host(W0))&setIn(Z,alive))&setIn(W0,alive))&index(status,host(W0))=elec_2)&leq(s(host(X)),index(pendack,host(W0))))))))))))))),
% 3.73/1.01 inference(miniscoping,[status(thm)],[f212])).
% 3.73/1.01 fof(f214,plain,(
% 3.73/1.01 ((((((((((((((![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z]: (~index(status,host(Z))=elec_2|~leq(index(pendack,host(Z)),host(Z)))))&(![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)))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_2)|(![Z]: ~elem(m_Ack(Z,Pid0),queue(host(Z)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~setIn(host(Pid0),index(down,host(Z))))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20]: ((![Pid0]: ((((leq(host(Pid0),host(Z))|~setIn(Z,alive))|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Pid0))=elec_2))|~elem(m_Down(Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20]: ((![Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid0]: (((![Pid20]: (((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Down(Pid20),queue(host(Z))))|~host(Pid0)=host(Pid20)))|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![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))))))&queue(host(sK4_skl))=cons(m_Down(sK5_skl),sK6_skl))&(setIn(sK4_skl,alive)&(~leq(host(sK4_skl),host(sK5_skl))&(((~index(ldr,host(sK4_skl))=host(sK5_skl)|~index(status,host(sK4_skl))=norm)&(~index(status,host(sK4_skl))=wait|~host(sK5_skl)=host(index(elid,host(sK4_skl)))))&(((![Z]: ((leq(host(sK4_skl),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(sK4_skl)))|Z=host(sK5_skl))))&index(status,host(sK4_skl))=elec_1)&(~leq(nbr_proc,host(sK4_skl))&(host(sK4_skl)=host(sK7_skl)&(~host(sK4_skl)=host(sK8_skl)&((((~leq(host(sK7_skl),host(sK8_skl))&setIn(sK7_skl,alive))&setIn(sK8_skl,alive))&index(status,host(sK8_skl))=elec_2)&leq(s(host(sK4_skl)),index(pendack,host(sK8_skl))))))))))))),
% 3.73/1.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(V,sK6_skl),skolemize(Z,sK7_skl),skolemize(W0,sK8_skl)],[f213])).
% 3.73/1.01 fof(f222,plain,(
% 3.73/1.01 ![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)))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f226,plain,(
% 3.73/1.01 ![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)))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f228,plain,(
% 3.73/1.01 queue(host(sK4_skl))=cons(m_Down(sK5_skl),sK6_skl)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f233,plain,(
% 3.73/1.01 ![X0]: (leq(host(sK4_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK4_skl)))|X0=host(sK5_skl))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f236,plain,(
% 3.73/1.01 host(sK4_skl)=host(sK7_skl)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f237,plain,(
% 3.73/1.01 ~host(sK4_skl)=host(sK8_skl)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f238,plain,(
% 3.73/1.01 ~leq(host(sK7_skl),host(sK8_skl))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f239,plain,(
% 3.73/1.01 setIn(sK7_skl,alive)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f240,plain,(
% 3.73/1.01 setIn(sK8_skl,alive)),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f241,plain,(
% 3.73/1.01 index(status,host(sK8_skl))=elec_2),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f242,plain,(
% 3.73/1.01 leq(s(host(sK4_skl)),index(pendack,host(sK8_skl)))),
% 3.73/1.01 inference(cnf_transformation,[status(thm)],[f214])).
% 3.73/1.01 fof(f257,plain,(
% 3.73/1.01 ![X0,X1]: (elem(X0,cons(X0,X1)))),
% 3.73/1.01 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 3.73/1.01 fof(f295,plain,(
% 3.73/1.01 ![X0]: (~leq(s(s(X0)),X0))),
% 3.73/1.01 inference(resolution,[status(thm)],[f210,f191])).
% 3.73/1.01 fof(f305,plain,(
% 3.73/1.01 queue(host(sK7_skl))=cons(m_Down(sK5_skl),sK6_skl)),
% 3.73/1.01 inference(backward_demodulation,[status(thm)],[f236,f228])).
% 3.73/1.01 fof(f355,definition,(
% 3.73/1.01 sQ16_spl <=> (index(status,host(sK8_skl))=elec_2)),
% 3.73/1.01 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 3.73/1.01 fof(f357,plain,(
% 3.73/1.01 ~index(status,host(sK8_skl))=elec_2|sQ16_spl),
% 3.73/1.01 inference(component_clause,[status(thm)],[f355])).
% 3.73/1.01 fof(f382,plain,(
% 3.73/1.01 leq(s(host(sK7_skl)),index(pendack,host(sK8_skl)))),
% 3.73/1.01 inference(forward_demodulation,[status(thm)],[f236,f242])).
% 3.73/1.01 fof(f409,plain,(
% 3.73/1.01 elem(m_Down(sK5_skl),queue(host(sK7_skl)))),
% 3.73/1.01 inference(paramodulation,[status(thm)],[f305,f257])).
% 3.73/1.01 fof(f443,plain,(
% 3.73/1.01 leq(host(sK8_skl),host(sK7_skl))),
% 3.73/1.01 inference(resolution,[status(thm)],[f193,f238])).
% 3.73/1.01 fof(f492,definition,(
% 3.73/1.01 sQ27_spl <=> (leq(index(pendack,host(sK8_skl)),host(sK7_skl)))),
% 3.73/1.01 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 3.73/1.01 fof(f493,plain,(
% 3.73/1.01 leq(index(pendack,host(sK8_skl)),host(sK7_skl))|~sQ27_spl),
% 3.73/1.01 inference(component_clause,[status(thm)],[f492])).
% 3.73/1.01 fof(f517,plain,(
% 3.73/1.01 ![X0,X1]: (~leq(s(X0),X1)|~leq(X1,X0))),
% 3.73/1.01 inference(resolution,[status(thm)],[f201,f191])).
% 3.73/1.01 fof(f565,definition,(
% 3.73/1.01 sQ36_spl <=> (setIn(sK7_skl,alive))),
% 3.73/1.01 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 3.73/1.01 fof(f567,plain,(
% 3.73/1.01 ~setIn(sK7_skl,alive)|sQ36_spl),
% 3.73/1.01 inference(component_clause,[status(thm)],[f565])).
% 3.73/1.01 fof(f569,plain,(
% 3.73/1.01 ![X0]: (~setIn(sK7_skl,alive)|~setIn(X0,alive)|~host(X0)=host(sK5_skl)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK7_skl)))),
% 3.73/1.01 inference(resolution,[status(thm)],[f226,f409])).
% 3.73/1.01 fof(f571,definition,(
% 3.73/1.01 ![X0]: (sQ37_spl <=> (~setIn(X0,alive)|~host(X0)=host(sK5_skl)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK7_skl))))),
% 3.73/1.01 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 3.73/1.01 fof(f572,plain,(
% 3.73/1.01 ![X0]: (~setIn(X0,alive)|~host(X0)=host(sK5_skl)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK7_skl))|~sQ37_spl)),
% 3.73/1.01 inference(component_clause,[status(thm)],[f571])).
% 3.73/1.01 fof(f574,plain,(
% 3.73/1.01 ~sQ36_spl|sQ37_spl),
% 3.73/1.01 inference(split_clause,[status(thm)],[f569,f565,f571])).
% 3.73/1.01 fof(f579,plain,(
% 3.73/1.01 $false|sQ36_spl),
% 3.73/1.01 inference(forward_subsumption_resolution,[status(thm)],[f567,f239])).
% 3.73/1.01 fof(f580,plain,(
% 3.73/1.01 sQ36_spl),
% 3.73/1.01 inference(contradiction_clause,[status(thm)],[f579])).
% 3.73/1.01 fof(f613,plain,(
% 3.73/1.01 ~elec_2=elec_2|sQ16_spl),
% 3.73/1.01 inference(forward_demodulation,[status(thm)],[f241,f357])).
% 3.73/1.01 fof(f614,plain,(
% 3.73/1.01 $false|sQ16_spl),
% 3.73/1.01 inference(trivial_equality_resolution,[status(thm)],[f613])).
% 3.73/1.01 fof(f615,plain,(
% 3.73/1.01 sQ16_spl),
% 3.73/1.01 inference(contradiction_clause,[status(thm)],[f614])).
% 3.73/1.01 fof(f616,plain,(
% 3.73/1.01 ![X0]: (leq(host(sK7_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK4_skl)))|X0=host(sK5_skl))),
% 3.73/1.01 inference(forward_demodulation,[status(thm)],[f236,f233])).
% 3.73/1.01 fof(f617,plain,(
% 3.73/1.01 ![X0]: (leq(host(sK7_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK7_skl)))|X0=host(sK5_skl))),
% 3.73/1.01 inference(forward_demodulation,[status(thm)],[f236,f616])).
% 3.73/1.01 fof(f618,plain,(
% 3.73/1.01 ![X0]: (leq(host(sK7_skl),host(X0))|~leq(s(zero),host(X0))|host(X0)=host(sK5_skl)|~setIn(sK7_skl,alive)|~setIn(X0,alive)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK7_skl)))),
% 3.73/1.01 inference(resolution,[status(thm)],[f617,f222])).
% 3.12/1.02 fof(f619,definition,(
% 3.12/1.02 ![X0]: (sQ42_spl <=> (leq(host(sK7_skl),host(X0))|~leq(s(zero),host(X0))|host(X0)=host(sK5_skl)|~setIn(X0,alive)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK7_skl))))),
% 3.12/1.02 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 3.12/1.02 fof(f620,plain,(
% 3.12/1.02 ![X0]: (leq(host(sK7_skl),host(X0))|~leq(s(zero),host(X0))|host(X0)=host(sK5_skl)|~setIn(X0,alive)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK7_skl))|~sQ42_spl)),
% 3.12/1.02 inference(component_clause,[status(thm)],[f619])).
% 3.12/1.02 fof(f622,plain,(
% 3.12/1.02 sQ42_spl|~sQ36_spl),
% 3.12/1.02 inference(split_clause,[status(thm)],[f618,f619,f565])).
% 3.12/1.02 fof(f623,plain,(
% 3.12/1.02 ![X0]: (leq(host(sK7_skl),host(X0))|host(X0)=host(sK5_skl)|~setIn(X0,alive)|~index(status,host(X0))=elec_2|leq(index(pendack,host(X0)),host(sK7_skl))|~sQ42_spl)),
% 3.12/1.02 inference(forward_subsumption_resolution,[status(thm)],[f620,f74])).
% 3.12/1.02 fof(f672,plain,(
% 3.12/1.02 ~host(sK7_skl)=host(sK8_skl)),
% 3.12/1.02 inference(forward_demodulation,[status(thm)],[f236,f237])).
% 3.12/1.02 fof(f704,plain,(
% 3.12/1.02 ~leq(host(sK7_skl),host(sK8_skl))|host(sK7_skl)=host(sK8_skl)),
% 3.12/1.02 inference(resolution,[status(thm)],[f443,f196])).
% 3.12/1.02 fof(f705,definition,(
% 3.12/1.02 sQ47_spl <=> (leq(host(sK7_skl),host(sK8_skl)))),
% 3.12/1.02 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 3.12/1.02 fof(f708,definition,(
% 3.12/1.02 sQ48_spl <=> (host(sK7_skl)=host(sK8_skl))),
% 3.12/1.02 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 3.12/1.02 fof(f709,plain,(
% 3.12/1.02 host(sK7_skl)=host(sK8_skl)|~sQ48_spl),
% 3.12/1.02 inference(component_clause,[status(thm)],[f708])).
% 3.12/1.02 fof(f711,plain,(
% 3.12/1.02 ~sQ47_spl|sQ48_spl),
% 3.12/1.02 inference(split_clause,[status(thm)],[f704,f705,f708])).
% 3.12/1.02 fof(f785,plain,(
% 3.12/1.02 $false|~sQ48_spl),
% 3.12/1.02 inference(forward_subsumption_resolution,[status(thm)],[f709,f672])).
% 3.12/1.02 fof(f786,plain,(
% 3.12/1.02 ~sQ48_spl),
% 3.12/1.02 inference(contradiction_clause,[status(thm)],[f785])).
% 3.12/1.02 fof(f929,plain,(
% 3.12/1.02 ~leq(index(pendack,host(sK8_skl)),host(sK7_skl))),
% 3.12/1.02 inference(resolution,[status(thm)],[f517,f382])).
% 3.12/1.02 fof(f1101,definition,(
% 3.12/1.02 sQ74_spl <=> (s(zero)=s(s(nbr_proc)))),
% 3.12/1.02 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 3.12/1.02 fof(f1102,plain,(
% 3.12/1.02 s(zero)=s(s(nbr_proc))|~sQ74_spl),
% 3.12/1.02 inference(component_clause,[status(thm)],[f1101])).
% 3.12/1.02 fof(f1674,plain,(
% 3.12/1.02 leq(host(sK7_skl),host(sK8_skl))|host(sK8_skl)=host(sK5_skl)|~index(status,host(sK8_skl))=elec_2|leq(index(pendack,host(sK8_skl)),host(sK7_skl))|~sQ42_spl),
% 3.12/1.02 inference(resolution,[status(thm)],[f623,f240])).
% 3.12/1.02 fof(f1676,definition,(
% 3.12/1.02 sQ110_spl <=> (host(sK8_skl)=host(sK5_skl))),
% 3.12/1.02 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 3.12/1.02 fof(f1679,plain,(
% 3.12/1.02 sQ47_spl|sQ110_spl|~sQ16_spl|sQ27_spl|~sQ42_spl),
% 3.12/1.02 inference(split_clause,[status(thm)],[f1674,f705,f1676,f355,f492,f619])).
% 3.12/1.02 fof(f3186,plain,(
% 3.12/1.02 $false|~sQ27_spl),
% 3.12/1.02 inference(forward_subsumption_resolution,[status(thm)],[f493,f929])).
% 3.12/1.02 fof(f3187,plain,(
% 3.12/1.02 ~sQ27_spl),
% 3.12/1.02 inference(contradiction_clause,[status(thm)],[f3186])).
% 3.12/1.02 fof(f3613,plain,(
% 3.12/1.02 ~leq(s(zero),nbr_proc)|~sQ74_spl),
% 3.12/1.02 inference(paramodulation,[status(thm)],[f1102,f295])).
% 3.12/1.02 fof(f3691,plain,(
% 3.12/1.02 $false|~sQ74_spl),
% 3.12/1.02 inference(forward_subsumption_resolution,[status(thm)],[f3613,f75])).
% 3.12/1.02 fof(f3692,plain,(
% 3.12/1.02 ~sQ74_spl),
% 3.12/1.02 inference(contradiction_clause,[status(thm)],[f3691])).
% 3.12/1.02 fof(f3999,plain,(
% 3.12/1.02 ~host(sK8_skl)=host(sK5_skl)|~index(status,host(sK8_skl))=elec_2|leq(index(pendack,host(sK8_skl)),host(sK7_skl))|~sQ37_spl),
% 3.12/1.02 inference(resolution,[status(thm)],[f572,f240])).
% 3.12/1.02 fof(f4001,plain,(
% 3.12/1.02 ~sQ110_spl|~sQ16_spl|sQ27_spl|~sQ37_spl),
% 3.12/1.02 inference(split_clause,[status(thm)],[f3999,f1676,f355,f492,f571])).
% 3.12/1.02 fof(f4003,plain,(
% 3.12/1.02 $false),
% 3.12/1.02 inference(sat_refutation,[status(thm)],[f574,f580,f615,f622,f711,f786,f1679,f3187,f3692,f4001])).
% 3.12/1.02 % SZS output end CNFRefutation for theBenchmark.p
% 3.12/1.03 % Elapsed time: 0.652435 seconds
% 3.12/1.03 % CPU time: 4.807141 seconds
% 3.12/1.03 % Total memory used: 158.667 MB
% 3.12/1.03 % Net memory used: 148.739 MB
%------------------------------------------------------------------------------