%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV461+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:53 PM UTC 2026
% Result : Theorem 11.16s 1.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV461+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:53:32 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 11.16/1.86 % Refutation found
% 11.16/1.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.16/1.86 % SZS output start CNFRefutation for theBenchmark
% 11.16/1.86 fof(f5,axiom,(
% 11.16/1.86 (! [P] : leq(host(P),nbr_proc) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f12,axiom,(
% 11.16/1.86 (! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f18,axiom,(
% 11.16/1.86 (! [X,Y] : m_Down(X) != m_Halt(Y) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f48,axiom,(
% 11.16/1.86 (! [X,Y,Q] :( elem(X,snoc(Q,Y))<=> ( X = Y| elem(X,Q) ) ) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f59,axiom,(
% 11.16/1.86 (! [X] : ~ leq(s(X),X) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f60,axiom,(
% 11.16/1.86 (! [X] : leq(X,X) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f62,axiom,(
% 11.16/1.86 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f67,conjecture,(
% 11.16/1.86 (! [V,W] :( ( (! [X] :( host(W) = host(X)=> ~ setIn(X,alive) ))& (! [X,Y] :( elem(m_Ldr(Y),queue(host(X)))=> ~ leq(host(X),host(Y)) ))& (! [X,Y] :( elem(m_Down(Y),queue(host(X)))=> host(Y) != host(X) ))& (! [X,Y] :( elem(m_Halt(Y),queue(host(X)))=> ~ leq(host(X),host(Y)) ))& (! [X,Y,Z] :( elem(m_Ack(Z,X),queue(host(Y)))=> ~ leq(host(X),host(Z)) ))& (! [X,Y] :( ( Y != X& host(Y) = host(X) )=> ( ~ setIn(X,alive)| ~ setIn(Y,alive) ) ))& (! [X,Y] :( ( setIn(Y,alive)& elem(m_Ack(Y,X),queue(host(Y))) )=> leq(host(X),index(pendack,host(Y))) ))& (! [X,Y] :( ( setIn(Y,alive)& index(status,host(Y)) = elec_1 )=> ~ elem(m_Ack(Y,X),queue(host(Y))) ))& (! [X] :( ( ( index(status,host(X)) = elec_1| index(status,host(X)) = elec_2 )& setIn(X,alive) )=> index(elid,host(X)) = X ))& (! [X,Y,Z] :( ( setIn(Z,alive)& elem(m_Down(Y),queue(host(Z)))& host(Y) = host(X) )=> ~ ( setIn(X,alive)& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ))& (! [X,Y,Z] :( ( setIn(X,alive)& setIn(Z,alive)& host(Z) = host(Y)& index(status,host(X)) = elec_2& index(status,host(Z)) = elec_2 )=> ~ elem(m_Ack(X,Y),queue(host(X))) ))& (! [X,Y] :( ( ~ leq(host(X),host(Y))& setIn(X,alive)& setIn(Y,alive)& index(status,host(X)) = elec_2& index(status,host(Y)) = elec_2 )=> leq(index(pendack,host(Y)),host(X)) ))& (! [X,Y] :( ( ~ leq(host(X),host(Y))& setIn(X,alive)& setIn(Y,alive)& index(status,host(X)) = elec_2& index(status,host(Y)) = elec_2 )=> ~ leq(index(pendack,host(X)),index(pendack,host(Y))) ))& (! [X,Y,Z] :( ( ~ leq(index(pendack,host(Z)),host(X))& setIn(Z,alive)& elem(m_Halt(Z),queue(host(Y)))& index(status,host(Z)) = elec_2 )=> ~ ( setIn(X,alive)& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ))& (! [X,Y,Z,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Z) ) ))& elem(m_Down(Z),queue(host(Pid0)))& host(Pid0) = host(Y)& host(Pid0) = nbr_proc& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(X,alive)& elem(m_Down(Y),queue(host(X))) ) ))& (! [X,Y,Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& elem(m_Ack(Pid0,Y),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Y) = index(pendack,host(Pid0))& host(Z) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(X,alive)& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ) ))=> ( queue(host(W)) = q_nil=> ( ( (! [X] :( host(W) = host(X)=> leq(X,V) ))& ~ setIn(V,pids)& host(W) = host(V) )=> ( host(V) = s(zero)=> ( ~ leq(nbr_proc,host(V))=> (! [X] :( host(V) != host(X)=> (! [Y,Z,Z0] :( s(host(V)) = host(Z0)=> ( host(V) != host(Z0)=> ( ( ( setIn(Z0,alive)| Z0 = V )& leq(nbr_proc,s(index(pendack,host(Z0))))& elem(m_Down(Z),snoc(queue(host(Z0)),m_Halt(V)))& elem(m_Ack(Z0,Y),snoc(queue(host(Z0)),m_Halt(V)))& index(status,host(Z0)) = elec_2& host(Y) = index(pendack,host(Z0))& host(Z) = s(index(pendack,host(Z0))) )=> ~ ( ( setIn(X,alive)| X = V )& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ) ) ) )) )) ) ) ) ) )),
% 11.16/1.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.16/1.86 fof(f68,negated_conjecture,(
% 11.16/1.86 ~((! [V,W] :( ( (! [X] :( host(W) = host(X)=> ~ setIn(X,alive) ))& (! [X,Y] :( elem(m_Ldr(Y),queue(host(X)))=> ~ leq(host(X),host(Y)) ))& (! [X,Y] :( elem(m_Down(Y),queue(host(X)))=> host(Y) != host(X) ))& (! [X,Y] :( elem(m_Halt(Y),queue(host(X)))=> ~ leq(host(X),host(Y)) ))& (! [X,Y,Z] :( elem(m_Ack(Z,X),queue(host(Y)))=> ~ leq(host(X),host(Z)) ))& (! [X,Y] :( ( Y != X& host(Y) = host(X) )=> ( ~ setIn(X,alive)| ~ setIn(Y,alive) ) ))& (! [X,Y] :( ( setIn(Y,alive)& elem(m_Ack(Y,X),queue(host(Y))) )=> leq(host(X),index(pendack,host(Y))) ))& (! [X,Y] :( ( setIn(Y,alive)& index(status,host(Y)) = elec_1 )=> ~ elem(m_Ack(Y,X),queue(host(Y))) ))& (! [X] :( ( ( index(status,host(X)) = elec_1| index(status,host(X)) = elec_2 )& setIn(X,alive) )=> index(elid,host(X)) = X ))& (! [X,Y,Z] :( ( setIn(Z,alive)& elem(m_Down(Y),queue(host(Z)))& host(Y) = host(X) )=> ~ ( setIn(X,alive)& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ))& (! [X,Y,Z] :( ( setIn(X,alive)& setIn(Z,alive)& host(Z) = host(Y)& index(status,host(X)) = elec_2& index(status,host(Z)) = elec_2 )=> ~ elem(m_Ack(X,Y),queue(host(X))) ))& (! [X,Y] :( ( ~ leq(host(X),host(Y))& setIn(X,alive)& setIn(Y,alive)& index(status,host(X)) = elec_2& index(status,host(Y)) = elec_2 )=> leq(index(pendack,host(Y)),host(X)) ))& (! [X,Y] :( ( ~ leq(host(X),host(Y))& setIn(X,alive)& setIn(Y,alive)& index(status,host(X)) = elec_2& index(status,host(Y)) = elec_2 )=> ~ leq(index(pendack,host(X)),index(pendack,host(Y))) ))& (! [X,Y,Z] :( ( ~ leq(index(pendack,host(Z)),host(X))& setIn(Z,alive)& elem(m_Halt(Z),queue(host(Y)))& index(status,host(Z)) = elec_2 )=> ~ ( setIn(X,alive)& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ))& (! [X,Y,Z,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Z) ) ))& elem(m_Down(Z),queue(host(Pid0)))& host(Pid0) = host(Y)& host(Pid0) = nbr_proc& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(X,alive)& elem(m_Down(Y),queue(host(X))) ) ))& (! [X,Y,Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& elem(m_Ack(Pid0,Y),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Y) = index(pendack,host(Pid0))& host(Z) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(X,alive)& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ) ))=> ( queue(host(W)) = q_nil=> ( ( (! [X] :( host(W) = host(X)=> leq(X,V) ))& ~ setIn(V,pids)& host(W) = host(V) )=> ( host(V) = s(zero)=> ( ~ leq(nbr_proc,host(V))=> (! [X] :( host(V) != host(X)=> (! [Y,Z,Z0] :( s(host(V)) = host(Z0)=> ( host(V) != host(Z0)=> ( ( ( setIn(Z0,alive)| Z0 = V )& leq(nbr_proc,s(index(pendack,host(Z0))))& elem(m_Down(Z),snoc(queue(host(Z0)),m_Halt(V)))& elem(m_Ack(Z0,Y),snoc(queue(host(Z0)),m_Halt(V)))& index(status,host(Z0)) = elec_2& host(Y) = index(pendack,host(Z0))& host(Z) = s(index(pendack,host(Z0))) )=> ~ ( ( setIn(X,alive)| X = V )& index(ldr,host(X)) = host(X)& index(status,host(X)) = norm ) ) ) ) )) )) ) ) ) ) ))),
% 11.16/1.86 inference(negated_conjecture,[status(cth)],[f67])).
% 11.16/1.86 fof(f76,plain,(
% 11.16/1.86 ![X0]: (leq(host(X0),nbr_proc))),
% 11.16/1.86 inference(cnf_transformation,[status(thm)],[f5])).
% 11.16/1.86 fof(f83,plain,(
% 11.16/1.86 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_Halt(X2))),
% 11.16/1.86 inference(cnf_transformation,[status(thm)],[f12])).
% 11.16/1.86 fof(f89,plain,(
% 11.16/1.86 ![X0,X1]: (~m_Down(X0)=m_Halt(X1))),
% 11.16/1.86 inference(cnf_transformation,[status(thm)],[f18])).
% 11.16/1.86 fof(f143,plain,(
% 11.16/1.86 ![X,Y,Q]: ((~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q)))&(elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 11.16/1.86 inference(NNF_transformation,[status(thm)],[f48])).
% 11.16/1.86 fof(f144,plain,(
% 11.16/1.86 (![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))))),
% 11.16/1.86 inference(miniscoping,[status(thm)],[f143])).
% 11.16/1.86 fof(f145,plain,(
% 11.16/1.86 ![X0,X1,X2]: (~elem(X0,snoc(X1,X2))|X0=X2|elem(X0,X1))),
% 11.16/1.86 inference(cnf_transformation,[status(thm)],[f144])).
% 11.16/1.86 fof(f191,plain,(
% 11.16/1.86 ![X0]: (~leq(s(X0),X0))),
% 11.16/1.86 inference(cnf_transformation,[status(thm)],[f59])).
% 11.16/1.86 fof(f192,plain,(
% 11.16/1.86 ![X0]: (leq(X0,X0))),
% 11.16/1.86 inference(cnf_transformation,[status(thm)],[f60])).
% 11.16/1.86 fof(f194,plain,(
% 11.16/1.86 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 11.16/1.86 inference(NNF_transformation,[status(thm)],[f62])).
% 11.16/1.86 fof(f195,plain,(
% 11.16/1.86 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 11.16/1.86 inference(miniscoping,[status(thm)],[f194])).
% 11.16/1.86 fof(f196,plain,(
% 11.16/1.86 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 11.16/1.86 inference(cnf_transformation,[status(thm)],[f195])).
% 11.16/1.86 fof(f212,plain,(
% 11.16/1.86 (?[V,W]: (((((((((((((((((![X]: (~host(W)=host(X)|~setIn(X,alive)))&(![X,Y]: (~elem(m_Ldr(Y),queue(host(X)))|~leq(host(X),host(Y)))))&(![X,Y]: (~elem(m_Down(Y),queue(host(X)))|~host(Y)=host(X))))&(![X,Y]: (~elem(m_Halt(Y),queue(host(X)))|~leq(host(X),host(Y)))))&(![X,Y,Z]: (~elem(m_Ack(Z,X),queue(host(Y)))|~leq(host(X),host(Z)))))&(![X,Y]: ((Y=X|~host(Y)=host(X))|(~setIn(X,alive)|~setIn(Y,alive)))))&(![X,Y]: ((~setIn(Y,alive)|~elem(m_Ack(Y,X),queue(host(Y))))|leq(host(X),index(pendack,host(Y))))))&(![X,Y]: ((~setIn(Y,alive)|~index(status,host(Y))=elec_1)|~elem(m_Ack(Y,X),queue(host(Y))))))&(![X]: (((~index(status,host(X))=elec_1&~index(status,host(X))=elec_2)|~setIn(X,alive))|index(elid,host(X))=X)))&(![X,Y,Z]: (((~setIn(Z,alive)|~elem(m_Down(Y),queue(host(Z))))|~host(Y)=host(X))|((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(![X,Y,Z]: (((((~setIn(X,alive)|~setIn(Z,alive))|~host(Z)=host(Y))|~index(status,host(X))=elec_2)|~index(status,host(Z))=elec_2)|~elem(m_Ack(X,Y),queue(host(X))))))&(![X,Y]: (((((leq(host(X),host(Y))|~setIn(X,alive))|~setIn(Y,alive))|~index(status,host(X))=elec_2)|~index(status,host(Y))=elec_2)|leq(index(pendack,host(Y)),host(X)))))&(![X,Y]: (((((leq(host(X),host(Y))|~setIn(X,alive))|~setIn(Y,alive))|~index(status,host(X))=elec_2)|~index(status,host(Y))=elec_2)|~leq(index(pendack,host(X)),index(pendack,host(Y))))))&(![X,Y,Z]: ((((leq(index(pendack,host(Z)),host(X))|~setIn(Z,alive))|~elem(m_Halt(Z),queue(host(Y))))|~index(status,host(Z))=elec_2)|((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(![X,Y,Z,Pid0]: ((((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Z))))|~elem(m_Down(Z),queue(host(Pid0))))|~host(Pid0)=host(Y))|~host(Pid0)=nbr_proc)|~index(status,host(Pid0))=elec_1)|(~setIn(X,alive)|~elem(m_Down(Y),queue(host(X)))))))&(![X,Y,Z,Pid0]: (((((((~setIn(Pid0,alive)|~elem(m_Down(Z),queue(host(Pid0))))|~elem(m_Ack(Pid0,Y),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Y)=index(pendack,host(Pid0)))|~host(Z)=s(index(pendack,host(Pid0))))|((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(queue(host(W))=q_nil&((((![X]: (~host(W)=host(X)|leq(X,V)))&~setIn(V,pids))&host(W)=host(V))&(host(V)=s(zero)&(~leq(nbr_proc,host(V))&(?[X]: (~host(V)=host(X)&(?[Y,Z,Z0]: (s(host(V))=host(Z0)&(~host(V)=host(Z0)&((((((((setIn(Z0,alive)|Z0=V)&leq(nbr_proc,s(index(pendack,host(Z0)))))&elem(m_Down(Z),snoc(queue(host(Z0)),m_Halt(V))))&elem(m_Ack(Z0,Y),snoc(queue(host(Z0)),m_Halt(V))))&index(status,host(Z0))=elec_2)&host(Y)=index(pendack,host(Z0)))&host(Z)=s(index(pendack,host(Z0))))&(((setIn(X,alive)|X=V)&index(ldr,host(X))=host(X))&index(status,host(X))=norm)))))))))))))),
% 11.16/1.86 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 11.16/1.86 fof(f213,plain,(
% 11.16/1.86 ?[W]: (((((((((((((((((![X]: (~host(W)=host(X)|~setIn(X,alive)))&(![X,Y]: (~elem(m_Ldr(Y),queue(host(X)))|~leq(host(X),host(Y)))))&(![X,Y]: (~elem(m_Down(Y),queue(host(X)))|~host(Y)=host(X))))&(![X,Y]: (~elem(m_Halt(Y),queue(host(X)))|~leq(host(X),host(Y)))))&(![X,Z]: ((![Y]: ~elem(m_Ack(Z,X),queue(host(Y))))|~leq(host(X),host(Z)))))&(![X,Y]: ((Y=X|~host(Y)=host(X))|(~setIn(X,alive)|~setIn(Y,alive)))))&(![X,Y]: ((~setIn(Y,alive)|~elem(m_Ack(Y,X),queue(host(Y))))|leq(host(X),index(pendack,host(Y))))))&(![Y]: ((~setIn(Y,alive)|~index(status,host(Y))=elec_1)|(![X]: ~elem(m_Ack(Y,X),queue(host(Y)))))))&(![X]: (((~index(status,host(X))=elec_1&~index(status,host(X))=elec_2)|~setIn(X,alive))|index(elid,host(X))=X)))&(![X]: ((![Y]: ((![Z]: (~setIn(Z,alive)|~elem(m_Down(Y),queue(host(Z)))))|~host(Y)=host(X)))|((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(![X,Y]: ((![Z]: ((((~setIn(X,alive)|~setIn(Z,alive))|~host(Z)=host(Y))|~index(status,host(X))=elec_2)|~index(status,host(Z))=elec_2))|~elem(m_Ack(X,Y),queue(host(X))))))&(![X,Y]: (((((leq(host(X),host(Y))|~setIn(X,alive))|~setIn(Y,alive))|~index(status,host(X))=elec_2)|~index(status,host(Y))=elec_2)|leq(index(pendack,host(Y)),host(X)))))&(![X,Y]: (((((leq(host(X),host(Y))|~setIn(X,alive))|~setIn(Y,alive))|~index(status,host(X))=elec_2)|~index(status,host(Y))=elec_2)|~leq(index(pendack,host(X)),index(pendack,host(Y))))))&(![X]: ((![Z]: (((leq(index(pendack,host(Z)),host(X))|~setIn(Z,alive))|(![Y]: ~elem(m_Halt(Z),queue(host(Y)))))|~index(status,host(Z))=elec_2))|((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(![Y]: ((![Pid0]: ((((![Z]: ((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Z))))|~elem(m_Down(Z),queue(host(Pid0)))))|~host(Pid0)=host(Y))|~host(Pid0)=nbr_proc)|~index(status,host(Pid0))=elec_1))|(![X]: (~setIn(X,alive)|~elem(m_Down(Y),queue(host(X))))))))&((![Z,Pid0]: ((![Y]: (((((~setIn(Pid0,alive)|~elem(m_Down(Z),queue(host(Pid0))))|~elem(m_Ack(Pid0,Y),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Y)=index(pendack,host(Pid0))))|~host(Z)=s(index(pendack,host(Pid0)))))|(![X]: ((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(queue(host(W))=q_nil&(?[V]: ((((![X]: (~host(W)=host(X)|leq(X,V)))&~setIn(V,pids))&host(W)=host(V))&(host(V)=s(zero)&(~leq(nbr_proc,host(V))&(?[X]: (~host(V)=host(X)&(?[Z0]: (s(host(V))=host(Z0)&(~host(V)=host(Z0)&((?[Z]: ((?[Y]: ((((((setIn(Z0,alive)|Z0=V)&leq(nbr_proc,s(index(pendack,host(Z0)))))&elem(m_Down(Z),snoc(queue(host(Z0)),m_Halt(V))))&elem(m_Ack(Z0,Y),snoc(queue(host(Z0)),m_Halt(V))))&index(status,host(Z0))=elec_2)&host(Y)=index(pendack,host(Z0))))&host(Z)=s(index(pendack,host(Z0)))))&(((setIn(X,alive)|X=V)&index(ldr,host(X))=host(X))&index(status,host(X))=norm)))))))))))))),
% 11.16/1.86 inference(miniscoping,[status(thm)],[f212])).
% 11.16/1.86 fof(f214,plain,(
% 11.16/1.86 (((((((((((((((((![X]: (~host(sK4_skl)=host(X)|~setIn(X,alive)))&(![X,Y]: (~elem(m_Ldr(Y),queue(host(X)))|~leq(host(X),host(Y)))))&(![X,Y]: (~elem(m_Down(Y),queue(host(X)))|~host(Y)=host(X))))&(![X,Y]: (~elem(m_Halt(Y),queue(host(X)))|~leq(host(X),host(Y)))))&(![X,Z]: ((![Y]: ~elem(m_Ack(Z,X),queue(host(Y))))|~leq(host(X),host(Z)))))&(![X,Y]: ((Y=X|~host(Y)=host(X))|(~setIn(X,alive)|~setIn(Y,alive)))))&(![X,Y]: ((~setIn(Y,alive)|~elem(m_Ack(Y,X),queue(host(Y))))|leq(host(X),index(pendack,host(Y))))))&(![Y]: ((~setIn(Y,alive)|~index(status,host(Y))=elec_1)|(![X]: ~elem(m_Ack(Y,X),queue(host(Y)))))))&(![X]: (((~index(status,host(X))=elec_1&~index(status,host(X))=elec_2)|~setIn(X,alive))|index(elid,host(X))=X)))&(![X]: ((![Y]: ((![Z]: (~setIn(Z,alive)|~elem(m_Down(Y),queue(host(Z)))))|~host(Y)=host(X)))|((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(![X,Y]: ((![Z]: ((((~setIn(X,alive)|~setIn(Z,alive))|~host(Z)=host(Y))|~index(status,host(X))=elec_2)|~index(status,host(Z))=elec_2))|~elem(m_Ack(X,Y),queue(host(X))))))&(![X,Y]: (((((leq(host(X),host(Y))|~setIn(X,alive))|~setIn(Y,alive))|~index(status,host(X))=elec_2)|~index(status,host(Y))=elec_2)|leq(index(pendack,host(Y)),host(X)))))&(![X,Y]: (((((leq(host(X),host(Y))|~setIn(X,alive))|~setIn(Y,alive))|~index(status,host(X))=elec_2)|~index(status,host(Y))=elec_2)|~leq(index(pendack,host(X)),index(pendack,host(Y))))))&(![X]: ((![Z]: (((leq(index(pendack,host(Z)),host(X))|~setIn(Z,alive))|(![Y]: ~elem(m_Halt(Z),queue(host(Y)))))|~index(status,host(Z))=elec_2))|((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(![Y]: ((![Pid0]: ((((![Z]: (((~leq(host(Pid0),sK5_skl(Z,Pid0,Y))&leq(s(zero),sK5_skl(Z,Pid0,Y)))&(~setIn(sK5_skl(Z,Pid0,Y),index(down,host(Pid0)))&~sK5_skl(Z,Pid0,Y)=host(Z)))|~elem(m_Down(Z),queue(host(Pid0)))))|~host(Pid0)=host(Y))|~host(Pid0)=nbr_proc)|~index(status,host(Pid0))=elec_1))|(![X]: (~setIn(X,alive)|~elem(m_Down(Y),queue(host(X))))))))&((![Z,Pid0]: ((![Y]: (((((~setIn(Pid0,alive)|~elem(m_Down(Z),queue(host(Pid0))))|~elem(m_Ack(Pid0,Y),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Y)=index(pendack,host(Pid0))))|~host(Z)=s(index(pendack,host(Pid0)))))|(![X]: ((~setIn(X,alive)|~index(ldr,host(X))=host(X))|~index(status,host(X))=norm))))&(queue(host(sK4_skl))=q_nil&((((![X]: (~host(sK4_skl)=host(X)|leq(X,sK6_skl)))&~setIn(sK6_skl,pids))&host(sK4_skl)=host(sK6_skl))&(host(sK6_skl)=s(zero)&(~leq(nbr_proc,host(sK6_skl))&(~host(sK6_skl)=host(sK7_skl)&(s(host(sK6_skl))=host(sK8_skl)&(~host(sK6_skl)=host(sK8_skl)&((((((((setIn(sK8_skl,alive)|sK8_skl=sK6_skl)&leq(nbr_proc,s(index(pendack,host(sK8_skl)))))&elem(m_Down(sK9_skl),snoc(queue(host(sK8_skl)),m_Halt(sK6_skl))))&elem(m_Ack(sK8_skl,sK10_skl),snoc(queue(host(sK8_skl)),m_Halt(sK6_skl))))&index(status,host(sK8_skl))=elec_2)&host(sK10_skl)=index(pendack,host(sK8_skl)))&host(sK9_skl)=s(index(pendack,host(sK8_skl))))&(((setIn(sK7_skl,alive)|sK7_skl=sK6_skl)&index(ldr,host(sK7_skl))=host(sK7_skl))&index(status,host(sK7_skl))=norm))))))))))),
% 11.16/1.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(W,sK4_skl),skolemize(V0,sK5_skl(Z,Pid0,Y)),skolemize(V,sK6_skl),skolemize(X,sK7_skl),skolemize(Z0,sK8_skl),skolemize(Z,sK9_skl),skolemize(Y,sK10_skl)],[f213])).
% 11.16/1.87 fof(f234,plain,(
% 11.16/1.87 ![X0,X1,X2,X3]: (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))|~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f238,plain,(
% 11.16/1.87 host(sK4_skl)=host(sK6_skl)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f241,plain,(
% 11.16/1.87 ~host(sK6_skl)=host(sK7_skl)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f242,plain,(
% 11.16/1.87 s(host(sK6_skl))=host(sK8_skl)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f243,plain,(
% 11.16/1.87 ~host(sK6_skl)=host(sK8_skl)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f244,plain,(
% 11.16/1.87 setIn(sK8_skl,alive)|sK8_skl=sK6_skl),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f245,plain,(
% 11.16/1.87 leq(nbr_proc,s(index(pendack,host(sK8_skl))))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f246,plain,(
% 11.16/1.87 elem(m_Down(sK9_skl),snoc(queue(host(sK8_skl)),m_Halt(sK6_skl)))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f247,plain,(
% 11.16/1.87 elem(m_Ack(sK8_skl,sK10_skl),snoc(queue(host(sK8_skl)),m_Halt(sK6_skl)))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f248,plain,(
% 11.16/1.87 index(status,host(sK8_skl))=elec_2),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f249,plain,(
% 11.16/1.87 host(sK10_skl)=index(pendack,host(sK8_skl))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f250,plain,(
% 11.16/1.87 host(sK9_skl)=s(index(pendack,host(sK8_skl)))),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f251,plain,(
% 11.16/1.87 setIn(sK7_skl,alive)|sK7_skl=sK6_skl),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f252,plain,(
% 11.16/1.87 index(ldr,host(sK7_skl))=host(sK7_skl)),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f253,plain,(
% 11.16/1.87 index(status,host(sK7_skl))=norm),
% 11.16/1.87 inference(cnf_transformation,[status(thm)],[f214])).
% 11.16/1.87 fof(f254,definition,(
% 11.16/1.87 ![X0,X1,X2]: (sQ0_spl <=> (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f255,plain,(
% 11.16/1.87 ![X0,X1,X2]: (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))|~sQ0_spl)),
% 11.16/1.87 inference(component_clause,[status(thm)],[f254])).
% 11.16/1.87 fof(f257,definition,(
% 11.16/1.87 ![X3]: (sQ1_spl <=> (~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f258,plain,(
% 11.16/1.87 ![X0]: (~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ1_spl)),
% 11.16/1.87 inference(component_clause,[status(thm)],[f257])).
% 11.16/1.87 fof(f260,plain,(
% 11.16/1.87 sQ0_spl|sQ1_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f234,f254,f257])).
% 11.16/1.87 fof(f261,definition,(
% 11.16/1.87 sQ2_spl <=> (setIn(sK8_skl,alive))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f264,definition,(
% 11.16/1.87 sQ3_spl <=> (sK8_skl=sK6_skl)),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f265,plain,(
% 11.16/1.87 sK8_skl=sK6_skl|~sQ3_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f264])).
% 11.16/1.87 fof(f267,plain,(
% 11.16/1.87 sQ2_spl|sQ3_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f244,f261,f264])).
% 11.16/1.87 fof(f268,definition,(
% 11.16/1.87 sQ4_spl <=> (setIn(sK7_skl,alive))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f269,plain,(
% 11.16/1.87 setIn(sK7_skl,alive)|~sQ4_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f268])).
% 11.16/1.87 fof(f271,definition,(
% 11.16/1.87 sQ5_spl <=> (sK7_skl=sK6_skl)),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f272,plain,(
% 11.16/1.87 sK7_skl=sK6_skl|~sQ5_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f271])).
% 11.16/1.87 fof(f274,plain,(
% 11.16/1.87 sQ4_spl|sQ5_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f251,f268,f271])).
% 11.16/1.87 fof(f288,plain,(
% 11.16/1.87 ~host(sK4_skl)=host(sK7_skl)),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f238,f241])).
% 11.16/1.87 fof(f289,plain,(
% 11.16/1.87 s(host(sK4_skl))=host(sK8_skl)),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f238,f242])).
% 11.16/1.87 fof(f290,plain,(
% 11.16/1.87 ~host(sK4_skl)=host(sK8_skl)),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f238,f243])).
% 11.16/1.87 fof(f291,plain,(
% 11.16/1.87 leq(nbr_proc,s(host(sK10_skl)))),
% 11.16/1.87 inference(backward_demodulation,[status(thm)],[f249,f245])).
% 11.16/1.87 fof(f292,plain,(
% 11.16/1.87 host(sK9_skl)=s(host(sK10_skl))),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f249,f250])).
% 11.16/1.87 fof(f293,plain,(
% 11.16/1.87 leq(nbr_proc,host(sK9_skl))),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f292,f291])).
% 11.16/1.87 fof(f374,plain,(
% 11.16/1.87 ~host(sK4_skl)=host(sK6_skl)|~sQ5_spl),
% 11.16/1.87 inference(backward_demodulation,[status(thm)],[f272,f288])).
% 11.16/1.87 fof(f380,plain,(
% 11.16/1.87 ~host(sK4_skl)=host(sK6_skl)|~sQ3_spl),
% 11.16/1.87 inference(backward_demodulation,[status(thm)],[f265,f290])).
% 11.16/1.87 fof(f550,plain,(
% 11.16/1.87 ~leq(host(sK9_skl),nbr_proc)|nbr_proc=host(sK9_skl)),
% 11.16/1.87 inference(resolution,[status(thm)],[f196,f293])).
% 11.16/1.87 fof(f578,definition,(
% 11.16/1.87 sQ28_spl <=> (leq(host(sK9_skl),nbr_proc))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f580,plain,(
% 11.16/1.87 ~leq(host(sK9_skl),nbr_proc)|sQ28_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f578])).
% 11.16/1.87 fof(f581,definition,(
% 11.16/1.87 sQ29_spl <=> (nbr_proc=host(sK9_skl))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f582,plain,(
% 11.16/1.87 nbr_proc=host(sK9_skl)|~sQ29_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f581])).
% 11.16/1.87 fof(f584,plain,(
% 11.16/1.87 ~sQ28_spl|sQ29_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f550,f578,f581])).
% 11.16/1.87 fof(f587,plain,(
% 11.16/1.87 $false|sQ28_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f580,f76])).
% 11.16/1.87 fof(f588,plain,(
% 11.16/1.87 sQ28_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f587])).
% 11.16/1.87 fof(f590,plain,(
% 11.16/1.87 nbr_proc=s(host(sK10_skl))|~sQ29_spl),
% 11.16/1.87 inference(backward_demodulation,[status(thm)],[f582,f292])).
% 11.16/1.87 fof(f639,definition,(
% 11.16/1.87 sQ35_spl <=> (index(status,host(sK8_skl))=elec_2)),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f641,plain,(
% 11.16/1.87 ~index(status,host(sK8_skl))=elec_2|sQ35_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f639])).
% 11.16/1.87 fof(f745,definition,(
% 11.16/1.87 sQ43_spl <=> (index(ldr,host(sK7_skl))=host(sK7_skl))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f747,plain,(
% 11.16/1.87 ~index(ldr,host(sK7_skl))=host(sK7_skl)|sQ43_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f745])).
% 11.16/1.87 fof(f748,definition,(
% 11.16/1.87 sQ44_spl <=> (index(status,host(sK7_skl))=norm)),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f750,plain,(
% 11.16/1.87 ~index(status,host(sK7_skl))=norm|sQ44_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f748])).
% 11.16/1.87 fof(f765,plain,(
% 11.16/1.87 ~norm=norm|sQ44_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f253,f750])).
% 11.16/1.87 fof(f766,plain,(
% 11.16/1.87 $false|sQ44_spl),
% 11.16/1.87 inference(trivial_equality_resolution,[status(thm)],[f765])).
% 11.16/1.87 fof(f767,plain,(
% 11.16/1.87 sQ44_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f766])).
% 11.16/1.87 fof(f768,plain,(
% 11.16/1.87 ~host(sK7_skl)=host(sK7_skl)|sQ43_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f252,f747])).
% 11.16/1.87 fof(f769,plain,(
% 11.16/1.87 $false|sQ43_spl),
% 11.16/1.87 inference(trivial_equality_resolution,[status(thm)],[f768])).
% 11.16/1.87 fof(f770,plain,(
% 11.16/1.87 sQ43_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f769])).
% 11.16/1.87 fof(f775,plain,(
% 11.16/1.87 ~host(sK4_skl)=host(sK4_skl)|~sQ5_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f238,f374])).
% 11.16/1.87 fof(f776,plain,(
% 11.16/1.87 $false|~sQ5_spl),
% 11.16/1.87 inference(trivial_equality_resolution,[status(thm)],[f775])).
% 11.16/1.87 fof(f777,plain,(
% 11.16/1.87 ~sQ5_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f776])).
% 11.16/1.87 fof(f882,plain,(
% 11.16/1.87 ~elec_2=elec_2|sQ35_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f248,f641])).
% 11.16/1.87 fof(f883,plain,(
% 11.16/1.87 $false|sQ35_spl),
% 11.16/1.87 inference(trivial_equality_resolution,[status(thm)],[f882])).
% 11.16/1.87 fof(f884,plain,(
% 11.16/1.87 sQ35_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f883])).
% 11.16/1.87 fof(f897,plain,(
% 11.16/1.87 ~host(sK4_skl)=host(sK4_skl)|~sQ3_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f238,f380])).
% 11.16/1.87 fof(f898,plain,(
% 11.16/1.87 $false|~sQ3_spl),
% 11.16/1.87 inference(trivial_equality_resolution,[status(thm)],[f897])).
% 11.16/1.87 fof(f899,plain,(
% 11.16/1.87 ~sQ3_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f898])).
% 11.16/1.87 fof(f1234,plain,(
% 11.16/1.87 ~leq(host(sK8_skl),host(sK4_skl))),
% 11.16/1.87 inference(paramodulation,[status(thm)],[f289,f191])).
% 11.16/1.87 fof(f1250,definition,(
% 11.16/1.87 ![X0]: (sQ110_spl <=> (~elem(m_Down(X0),queue(host(sK8_skl)))|~host(X0)=s(index(pendack,host(sK8_skl)))))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f1251,plain,(
% 11.16/1.87 ![X0]: (~elem(m_Down(X0),queue(host(sK8_skl)))|~host(X0)=s(index(pendack,host(sK8_skl)))|~sQ110_spl)),
% 11.16/1.87 inference(component_clause,[status(thm)],[f1250])).
% 11.16/1.87 fof(f1271,plain,(
% 11.16/1.87 ![X0]: (~elem(m_Down(X0),queue(host(sK8_skl)))|~host(X0)=s(host(sK10_skl))|~sQ110_spl)),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f249,f1251])).
% 11.16/1.87 fof(f1272,plain,(
% 11.16/1.87 ![X0]: (~elem(m_Down(X0),queue(host(sK8_skl)))|~host(X0)=nbr_proc|~sQ29_spl|~sQ110_spl)),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f590,f1271])).
% 11.16/1.87 fof(f1274,plain,(
% 11.16/1.87 m_Ack(sK8_skl,sK10_skl)=m_Halt(sK6_skl)|elem(m_Ack(sK8_skl,sK10_skl),queue(host(sK8_skl)))),
% 11.16/1.87 inference(resolution,[status(thm)],[f247,f145])).
% 11.16/1.87 fof(f1279,definition,(
% 11.16/1.87 sQ115_spl <=> (m_Ack(sK8_skl,sK10_skl)=m_Halt(sK6_skl))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f1280,plain,(
% 11.16/1.87 m_Ack(sK8_skl,sK10_skl)=m_Halt(sK6_skl)|~sQ115_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f1279])).
% 11.16/1.87 fof(f1282,definition,(
% 11.16/1.87 sQ116_spl <=> (elem(m_Ack(sK8_skl,sK10_skl),queue(host(sK8_skl))))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f1283,plain,(
% 11.16/1.87 elem(m_Ack(sK8_skl,sK10_skl),queue(host(sK8_skl)))|~sQ116_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f1282])).
% 11.16/1.87 fof(f1285,plain,(
% 11.16/1.87 sQ115_spl|sQ116_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f1274,f1279,f1282])).
% 11.16/1.87 fof(f1297,plain,(
% 11.16/1.87 $false|~sQ115_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f1280,f83])).
% 11.16/1.87 fof(f1298,plain,(
% 11.16/1.87 ~sQ115_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f1297])).
% 11.16/1.87 fof(f1300,plain,(
% 11.16/1.87 m_Down(sK9_skl)=m_Halt(sK6_skl)|elem(m_Down(sK9_skl),queue(host(sK8_skl)))),
% 11.16/1.87 inference(resolution,[status(thm)],[f246,f145])).
% 11.16/1.87 fof(f1306,definition,(
% 11.16/1.87 sQ120_spl <=> (m_Down(sK9_skl)=m_Halt(sK6_skl))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f1307,plain,(
% 11.16/1.87 m_Down(sK9_skl)=m_Halt(sK6_skl)|~sQ120_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f1306])).
% 11.16/1.87 fof(f1309,definition,(
% 11.16/1.87 sQ121_spl <=> (elem(m_Down(sK9_skl),queue(host(sK8_skl))))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f1310,plain,(
% 11.16/1.87 elem(m_Down(sK9_skl),queue(host(sK8_skl)))|~sQ121_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f1309])).
% 11.16/1.87 fof(f1312,plain,(
% 11.16/1.87 sQ120_spl|sQ121_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f1300,f1306,f1309])).
% 11.16/1.87 fof(f1326,plain,(
% 11.16/1.87 $false|~sQ120_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f1307,f89])).
% 11.16/1.87 fof(f1327,plain,(
% 11.16/1.87 ~sQ120_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f1326])).
% 11.16/1.87 fof(f1943,plain,(
% 11.16/1.87 ~index(ldr,host(sK7_skl))=host(sK7_skl)|~index(status,host(sK7_skl))=norm|~sQ1_spl|~sQ4_spl),
% 11.16/1.87 inference(resolution,[status(thm)],[f258,f269])).
% 11.16/1.87 fof(f1945,plain,(
% 11.16/1.87 ~sQ43_spl|~sQ44_spl|~sQ1_spl|~sQ4_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f1943,f745,f748,f257,f268])).
% 11.16/1.87 fof(f4847,plain,(
% 11.16/1.87 ![X0]: (~setIn(sK8_skl,alive)|~elem(m_Down(X0),queue(host(sK8_skl)))|~leq(nbr_proc,s(index(pendack,host(sK8_skl))))|~index(status,host(sK8_skl))=elec_2|~host(sK10_skl)=index(pendack,host(sK8_skl))|~host(X0)=s(index(pendack,host(sK8_skl)))|~sQ116_spl|~sQ0_spl)),
% 11.16/1.87 inference(resolution,[status(thm)],[f1283,f255])).
% 11.16/1.87 fof(f4864,definition,(
% 11.16/1.87 sQ241_spl <=> (leq(nbr_proc,s(index(pendack,host(sK8_skl)))))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f4866,plain,(
% 11.16/1.87 ~leq(nbr_proc,s(index(pendack,host(sK8_skl))))|sQ241_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f4864])).
% 11.16/1.87 fof(f4867,definition,(
% 11.16/1.87 sQ242_spl <=> (host(sK10_skl)=index(pendack,host(sK8_skl)))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f4869,plain,(
% 11.16/1.87 ~host(sK10_skl)=index(pendack,host(sK8_skl))|sQ242_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f4867])).
% 11.16/1.87 fof(f4870,plain,(
% 11.16/1.87 ~sQ2_spl|sQ110_spl|~sQ241_spl|~sQ35_spl|~sQ242_spl|~sQ116_spl|~sQ0_spl),
% 11.16/1.87 inference(split_clause,[status(thm)],[f4847,f261,f1250,f4864,f639,f4867,f1282,f254])).
% 11.16/1.87 fof(f4928,plain,(
% 11.16/1.87 ~host(sK10_skl)=host(sK10_skl)|sQ242_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f249,f4869])).
% 11.16/1.87 fof(f4929,plain,(
% 11.16/1.87 $false|sQ242_spl),
% 11.16/1.87 inference(trivial_equality_resolution,[status(thm)],[f4928])).
% 11.16/1.87 fof(f4930,plain,(
% 11.16/1.87 sQ242_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f4929])).
% 11.16/1.87 fof(f4931,plain,(
% 11.16/1.87 ~leq(nbr_proc,s(host(sK10_skl)))|sQ241_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f249,f4866])).
% 11.16/1.87 fof(f4932,plain,(
% 11.16/1.87 ~leq(nbr_proc,nbr_proc)|~sQ29_spl|sQ241_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f590,f4931])).
% 11.16/1.87 fof(f4933,plain,(
% 11.16/1.87 $false|~sQ29_spl|sQ241_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f4932,f192])).
% 11.16/1.87 fof(f4934,plain,(
% 11.16/1.87 ~sQ29_spl|sQ241_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f4933])).
% 11.16/1.87 fof(f5295,definition,(
% 11.16/1.87 sQ278_spl <=> (leq(host(sK8_skl),host(sK6_skl)))),
% 11.16/1.87 introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition])).
% 11.16/1.87 fof(f5296,plain,(
% 11.16/1.87 leq(host(sK8_skl),host(sK6_skl))|~sQ278_spl),
% 11.16/1.87 inference(component_clause,[status(thm)],[f5295])).
% 11.16/1.87 fof(f5299,plain,(
% 11.16/1.87 leq(host(sK8_skl),host(sK4_skl))|~sQ278_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f238,f5296])).
% 11.16/1.87 fof(f5300,plain,(
% 11.16/1.87 $false|~sQ278_spl),
% 11.16/1.87 inference(forward_subsumption_resolution,[status(thm)],[f5299,f1234])).
% 11.16/1.87 fof(f5301,plain,(
% 11.16/1.87 ~sQ278_spl),
% 11.16/1.87 inference(contradiction_clause,[status(thm)],[f5300])).
% 11.16/1.87 fof(f5656,plain,(
% 11.16/1.87 ~host(sK9_skl)=nbr_proc|~sQ121_spl|~sQ29_spl|~sQ110_spl),
% 11.16/1.87 inference(resolution,[status(thm)],[f1310,f1272])).
% 11.16/1.87 fof(f5683,plain,(
% 11.16/1.87 ~nbr_proc=nbr_proc|~sQ121_spl|~sQ29_spl|~sQ110_spl),
% 11.16/1.87 inference(forward_demodulation,[status(thm)],[f582,f5656])).
% 11.16/1.87 fof(f5684,plain,(
% 11.16/1.87 $false|~sQ121_spl|~sQ29_spl|~sQ110_spl),
% 11.16/1.87 inference(trivial_equality_resolution,[status(thm)],[f5683])).
% 11.16/1.88 fof(f5685,plain,(
% 11.16/1.88 ~sQ121_spl|~sQ29_spl|~sQ110_spl),
% 11.16/1.88 inference(contradiction_clause,[status(thm)],[f5684])).
% 11.16/1.88 fof(f5686,plain,(
% 11.16/1.88 $false),
% 11.16/1.88 inference(sat_refutation,[status(thm)],[f260,f267,f274,f584,f588,f767,f770,f777,f884,f899,f1285,f1298,f1312,f1327,f1945,f4870,f4930,f4934,f5301,f5685])).
% 11.16/1.88 % SZS output end CNFRefutation for theBenchmark.p
% 11.16/1.90 % Elapsed time: 1.533261 seconds
% 11.16/1.90 % CPU time: 11.721692 seconds
% 11.16/1.90 % Total memory used: 177.818 MB
% 11.16/1.90 % Net memory used: 164.995 MB
%------------------------------------------------------------------------------