%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV457+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 : n007.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 7.16s 1.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV457+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.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:50:20 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 7.16/1.50 % Refutation found
% 7.16/1.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.16/1.50 % SZS output start CNFRefutation for theBenchmark
% 7.16/1.50 fof(f5,axiom,(
% 7.16/1.50 (! [P] : leq(host(P),nbr_proc) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f32,axiom,(
% 7.16/1.50 (! [X1,X2,Y1,Y2] :( X1 != X2=> m_Ack(X1,Y1) != m_Ack(X2,Y2) ) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f33,axiom,(
% 7.16/1.50 (! [X1,X2,Y1,Y2] :( Y1 != Y2=> m_Ack(X1,Y1) != m_Ack(X2,Y2) ) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f47,axiom,(
% 7.16/1.50 (! [X,Y,Q] :( elem(X,cons(Y,Q))<=> ( X = Y| elem(X,Q) ) ) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f48,axiom,(
% 7.16/1.50 (! [X,Y,Q] :( elem(X,snoc(Q,Y))<=> ( X = Y| elem(X,Q) ) ) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f60,axiom,(
% 7.16/1.50 (! [X] : leq(X,X) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f62,axiom,(
% 7.16/1.50 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f67,conjecture,(
% 7.16/1.50 (! [V,W,X] :( ( (! [Y,Z] :( elem(m_Ack(Z,Y),queue(host(Z)))=> setIn(Z,pids) ))& (! [Y,Z] :( elem(m_Down(Z),queue(host(Y)))=> ~ setIn(Z,alive) ))& (! [Y,Z] :( elem(m_Ldr(Z),queue(host(Y)))=> ~ leq(host(Y),host(Z)) ))& (! [Y,Z,Pid0] :( elem(m_Ack(Pid0,Y),queue(host(Z)))=> ~ leq(host(Y),host(Pid0)) ))& (! [Y,Z] :( ( ~ setIn(Y,alive)& leq(Z,Y)& host(Z) = host(Y) )=> ~ setIn(Z,alive) ))& (! [Y,Z] :( ( Z != Y& host(Z) = host(Y) )=> ( ~ setIn(Y,alive)| ~ setIn(Z,alive) ) ))& (! [Y,Z] :( ( setIn(Z,alive)& elem(m_Ack(Z,Y),queue(host(Z))) )=> leq(host(Y),index(pendack,host(Z))) ))& (! [Y,Z] :( ( setIn(Z,alive)& index(status,host(Z)) = elec_1 )=> ~ elem(m_Ack(Y,Z),queue(host(Y))) ))& (! [Y,Z] :( ( setIn(Z,alive)& index(status,host(Z)) = elec_1 )=> ~ elem(m_Ack(Z,Y),queue(host(Z))) ))& (! [Y] :( ( ( index(status,host(Y)) = elec_1| index(status,host(Y)) = elec_2 )& setIn(Y,alive) )=> index(elid,host(Y)) = Y ))& (! [Y,Z,Pid0] :( ( elem(m_Down(Y),queue(host(Z)))& elem(m_Ack(Pid0,Z),queue(host(Pid0)))& host(Pid0) = host(Y) )=> ~ setIn(Pid0,alive) ))& (! [Y,Z,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& elem(m_Ack(Pid0,Y),queue(host(Pid0)))& host(Z) = host(Y) )=> ~ setIn(host(Pid0),index(down,host(Z))) ))& (! [Y,Z] :( ( ~ leq(host(Y),host(Z))& setIn(Y,alive)& setIn(Z,alive)& index(status,host(Y)) = elec_2& index(status,host(Z)) = elec_2 )=> ~ leq(index(pendack,host(Y)),index(pendack,host(Z))) ))& (! [Y,Z,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Y))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Z)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& (! [Y,Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0)))& leq(nbr_proc,index(pendack,host(Pid0)))& index(status,host(Pid0)) = elec_2& host(Z) = index(pendack,host(Pid0)) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& queue(host(W)) = cons(m_Halt(X),V) )=> ( setIn(W,alive)=> (! [Y] :( host(W) != host(Y)=> (! [Z,X0] :( host(X) = host(X0)=> ( host(W) != host(X0)=> ( ( setIn(X0,alive)& leq(nbr_proc,index(pendack,host(X0)))& elem(m_Ack(X0,Z),snoc(queue(host(X0)),m_Ack(X,W)))& index(status,host(X0)) = elec_2& host(Z) = index(pendack,host(X0)) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ) ) ) )) )) ) )),
% 7.16/1.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.16/1.50 fof(f68,negated_conjecture,(
% 7.16/1.50 ~((! [V,W,X] :( ( (! [Y,Z] :( elem(m_Ack(Z,Y),queue(host(Z)))=> setIn(Z,pids) ))& (! [Y,Z] :( elem(m_Down(Z),queue(host(Y)))=> ~ setIn(Z,alive) ))& (! [Y,Z] :( elem(m_Ldr(Z),queue(host(Y)))=> ~ leq(host(Y),host(Z)) ))& (! [Y,Z,Pid0] :( elem(m_Ack(Pid0,Y),queue(host(Z)))=> ~ leq(host(Y),host(Pid0)) ))& (! [Y,Z] :( ( ~ setIn(Y,alive)& leq(Z,Y)& host(Z) = host(Y) )=> ~ setIn(Z,alive) ))& (! [Y,Z] :( ( Z != Y& host(Z) = host(Y) )=> ( ~ setIn(Y,alive)| ~ setIn(Z,alive) ) ))& (! [Y,Z] :( ( setIn(Z,alive)& elem(m_Ack(Z,Y),queue(host(Z))) )=> leq(host(Y),index(pendack,host(Z))) ))& (! [Y,Z] :( ( setIn(Z,alive)& index(status,host(Z)) = elec_1 )=> ~ elem(m_Ack(Y,Z),queue(host(Y))) ))& (! [Y,Z] :( ( setIn(Z,alive)& index(status,host(Z)) = elec_1 )=> ~ elem(m_Ack(Z,Y),queue(host(Z))) ))& (! [Y] :( ( ( index(status,host(Y)) = elec_1| index(status,host(Y)) = elec_2 )& setIn(Y,alive) )=> index(elid,host(Y)) = Y ))& (! [Y,Z,Pid0] :( ( elem(m_Down(Y),queue(host(Z)))& elem(m_Ack(Pid0,Z),queue(host(Pid0)))& host(Pid0) = host(Y) )=> ~ setIn(Pid0,alive) ))& (! [Y,Z,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& elem(m_Ack(Pid0,Y),queue(host(Pid0)))& host(Z) = host(Y) )=> ~ setIn(host(Pid0),index(down,host(Z))) ))& (! [Y,Z] :( ( ~ leq(host(Y),host(Z))& setIn(Y,alive)& setIn(Z,alive)& index(status,host(Y)) = elec_2& index(status,host(Z)) = elec_2 )=> ~ leq(index(pendack,host(Y)),index(pendack,host(Z))) ))& (! [Y,Z,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Y))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Z)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& (! [Y,Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0)))& leq(nbr_proc,index(pendack,host(Pid0)))& index(status,host(Pid0)) = elec_2& host(Z) = index(pendack,host(Pid0)) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& queue(host(W)) = cons(m_Halt(X),V) )=> ( setIn(W,alive)=> (! [Y] :( host(W) != host(Y)=> (! [Z,X0] :( host(X) = host(X0)=> ( host(W) != host(X0)=> ( ( setIn(X0,alive)& leq(nbr_proc,index(pendack,host(X0)))& elem(m_Ack(X0,Z),snoc(queue(host(X0)),m_Ack(X,W)))& index(status,host(X0)) = elec_2& host(Z) = index(pendack,host(X0)) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ) ) ) )) )) ) ))),
% 7.16/1.50 inference(negated_conjecture,[status(cth)],[f67])).
% 7.16/1.50 fof(f76,plain,(
% 7.16/1.50 ![X0]: (leq(host(X0),nbr_proc))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f5])).
% 7.16/1.50 fof(f118,plain,(
% 7.16/1.50 ![X1,X2,Y1,Y2]: (X1=X2|~m_Ack(X1,Y1)=m_Ack(X2,Y2))),
% 7.16/1.50 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 7.16/1.50 fof(f119,plain,(
% 7.16/1.50 ![X1,X2]: (X1=X2|(![Y1,Y2]: ~m_Ack(X1,Y1)=m_Ack(X2,Y2)))),
% 7.16/1.50 inference(miniscoping,[status(thm)],[f118])).
% 7.16/1.50 fof(f120,plain,(
% 7.16/1.50 ![X0,X1,X2,X3]: (X0=X1|~m_Ack(X0,X2)=m_Ack(X1,X3))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f119])).
% 7.16/1.50 fof(f121,plain,(
% 7.16/1.50 ![X1,X2,Y1,Y2]: (Y1=Y2|~m_Ack(X1,Y1)=m_Ack(X2,Y2))),
% 7.16/1.50 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 7.16/1.50 fof(f122,plain,(
% 7.16/1.50 ![Y1,Y2]: (Y1=Y2|(![X1,X2]: ~m_Ack(X1,Y1)=m_Ack(X2,Y2)))),
% 7.16/1.50 inference(miniscoping,[status(thm)],[f121])).
% 7.16/1.50 fof(f123,plain,(
% 7.16/1.50 ![X0,X1,X2,X3]: (X0=X1|~m_Ack(X2,X0)=m_Ack(X3,X1))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f122])).
% 7.16/1.50 fof(f138,plain,(
% 7.16/1.50 ![X,Y,Q]: ((~elem(X,cons(Y,Q))|(X=Y|elem(X,Q)))&(elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 7.16/1.50 inference(NNF_transformation,[status(thm)],[f47])).
% 7.16/1.50 fof(f139,plain,(
% 7.16/1.50 (![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))))),
% 7.16/1.50 inference(miniscoping,[status(thm)],[f138])).
% 7.16/1.50 fof(f141,plain,(
% 7.16/1.50 ![X0,X1,X2]: (elem(X0,cons(X1,X2))|~X0=X1)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f139])).
% 7.16/1.50 fof(f143,plain,(
% 7.16/1.50 ![X,Y,Q]: ((~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q)))&(elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 7.16/1.50 inference(NNF_transformation,[status(thm)],[f48])).
% 7.16/1.50 fof(f144,plain,(
% 7.16/1.50 (![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))))),
% 7.16/1.50 inference(miniscoping,[status(thm)],[f143])).
% 7.16/1.50 fof(f145,plain,(
% 7.16/1.50 ![X0,X1,X2]: (~elem(X0,snoc(X1,X2))|X0=X2|elem(X0,X1))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f144])).
% 7.16/1.50 fof(f192,plain,(
% 7.16/1.50 ![X0]: (leq(X0,X0))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f60])).
% 7.16/1.50 fof(f194,plain,(
% 7.16/1.50 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 7.16/1.50 inference(NNF_transformation,[status(thm)],[f62])).
% 7.16/1.50 fof(f195,plain,(
% 7.16/1.50 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 7.16/1.50 inference(miniscoping,[status(thm)],[f194])).
% 7.16/1.50 fof(f196,plain,(
% 7.16/1.50 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f195])).
% 7.16/1.50 fof(f212,plain,(
% 7.16/1.50 (?[V,W,X]: (((((((((((((((((![Y,Z]: (~elem(m_Ack(Z,Y),queue(host(Z)))|setIn(Z,pids)))&(![Y,Z]: (~elem(m_Down(Z),queue(host(Y)))|~setIn(Z,alive))))&(![Y,Z]: (~elem(m_Ldr(Z),queue(host(Y)))|~leq(host(Y),host(Z)))))&(![Y,Z,Pid0]: (~elem(m_Ack(Pid0,Y),queue(host(Z)))|~leq(host(Y),host(Pid0)))))&(![Y,Z]: (((setIn(Y,alive)|~leq(Z,Y))|~host(Z)=host(Y))|~setIn(Z,alive))))&(![Y,Z]: ((Z=Y|~host(Z)=host(Y))|(~setIn(Y,alive)|~setIn(Z,alive)))))&(![Y,Z]: ((~setIn(Z,alive)|~elem(m_Ack(Z,Y),queue(host(Z))))|leq(host(Y),index(pendack,host(Z))))))&(![Y,Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|~elem(m_Ack(Y,Z),queue(host(Y))))))&(![Y,Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|~elem(m_Ack(Z,Y),queue(host(Z))))))&(![Y]: (((~index(status,host(Y))=elec_1&~index(status,host(Y))=elec_2)|~setIn(Y,alive))|index(elid,host(Y))=Y)))&(![Y,Z,Pid0]: (((~elem(m_Down(Y),queue(host(Z)))|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|~host(Pid0)=host(Y))|~setIn(Pid0,alive))))&(![Y,Z,Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Ack(Pid0,Y),queue(host(Pid0))))|~host(Z)=host(Y))|~setIn(host(Pid0),index(down,host(Z))))))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|~leq(index(pendack,host(Y)),index(pendack,host(Z))))))&(![Y,Z,Pid0]: ((((leq(index(pendack,host(Pid0)),host(Y))|~setIn(Pid0,alive))|~elem(m_Halt(Pid0),queue(host(Z))))|~index(status,host(Pid0))=elec_2)|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(![Y,Z,Pid0]: (((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Z)=index(pendack,host(Pid0)))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&queue(host(W))=cons(m_Halt(X),V))&(setIn(W,alive)&(?[Y]: (~host(W)=host(Y)&(?[Z,X0]: (host(X)=host(X0)&(~host(W)=host(X0)&(((((setIn(X0,alive)&leq(nbr_proc,index(pendack,host(X0))))&elem(m_Ack(X0,Z),snoc(queue(host(X0)),m_Ack(X,W))))&index(status,host(X0))=elec_2)&host(Z)=index(pendack,host(X0)))&((setIn(Y,alive)&index(ldr,host(Y))=host(Y))&index(status,host(Y))=norm))))))))))),
% 7.16/1.50 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 7.16/1.50 fof(f213,plain,(
% 7.16/1.50 ?[W,X]: (((((((((((((((((![Z]: ((![Y]: ~elem(m_Ack(Z,Y),queue(host(Z))))|setIn(Z,pids)))&(![Z]: ((![Y]: ~elem(m_Down(Z),queue(host(Y))))|~setIn(Z,alive))))&(![Y,Z]: (~elem(m_Ldr(Z),queue(host(Y)))|~leq(host(Y),host(Z)))))&(![Y,Pid0]: ((![Z]: ~elem(m_Ack(Pid0,Y),queue(host(Z))))|~leq(host(Y),host(Pid0)))))&(![Z]: ((![Y]: ((setIn(Y,alive)|~leq(Z,Y))|~host(Z)=host(Y)))|~setIn(Z,alive))))&(![Y,Z]: ((Z=Y|~host(Z)=host(Y))|(~setIn(Y,alive)|~setIn(Z,alive)))))&(![Y,Z]: ((~setIn(Z,alive)|~elem(m_Ack(Z,Y),queue(host(Z))))|leq(host(Y),index(pendack,host(Z))))))&(![Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|(![Y]: ~elem(m_Ack(Y,Z),queue(host(Y)))))))&(![Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|(![Y]: ~elem(m_Ack(Z,Y),queue(host(Z)))))))&(![Y]: (((~index(status,host(Y))=elec_1&~index(status,host(Y))=elec_2)|~setIn(Y,alive))|index(elid,host(Y))=Y)))&(![Pid0]: ((![Y]: ((![Z]: (~elem(m_Down(Y),queue(host(Z)))|~elem(m_Ack(Pid0,Z),queue(host(Pid0)))))|~host(Pid0)=host(Y)))|~setIn(Pid0,alive))))&(![Z,Pid0]: ((![Y]: (((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Ack(Pid0,Y),queue(host(Pid0))))|~host(Z)=host(Y)))|~setIn(host(Pid0),index(down,host(Z))))))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|~leq(index(pendack,host(Y)),index(pendack,host(Z))))))&(![Y]: ((![Pid0]: (((leq(index(pendack,host(Pid0)),host(Y))|~setIn(Pid0,alive))|(![Z]: ~elem(m_Halt(Pid0),queue(host(Z)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&((![Z,Pid0]: ((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Z)=index(pendack,host(Pid0))))|(![Y]: ((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(?[V]: queue(host(W))=cons(m_Halt(X),V)))&(setIn(W,alive)&(?[Y]: (~host(W)=host(Y)&(?[X0]: (host(X)=host(X0)&(~host(W)=host(X0)&((?[Z]: ((((setIn(X0,alive)&leq(nbr_proc,index(pendack,host(X0))))&elem(m_Ack(X0,Z),snoc(queue(host(X0)),m_Ack(X,W))))&index(status,host(X0))=elec_2)&host(Z)=index(pendack,host(X0))))&((setIn(Y,alive)&index(ldr,host(Y))=host(Y))&index(status,host(Y))=norm)))))))))),
% 7.16/1.50 inference(miniscoping,[status(thm)],[f212])).
% 7.16/1.50 fof(f214,plain,(
% 7.16/1.50 (((((((((((((((((![Z]: ((![Y]: ~elem(m_Ack(Z,Y),queue(host(Z))))|setIn(Z,pids)))&(![Z]: ((![Y]: ~elem(m_Down(Z),queue(host(Y))))|~setIn(Z,alive))))&(![Y,Z]: (~elem(m_Ldr(Z),queue(host(Y)))|~leq(host(Y),host(Z)))))&(![Y,Pid0]: ((![Z]: ~elem(m_Ack(Pid0,Y),queue(host(Z))))|~leq(host(Y),host(Pid0)))))&(![Z]: ((![Y]: ((setIn(Y,alive)|~leq(Z,Y))|~host(Z)=host(Y)))|~setIn(Z,alive))))&(![Y,Z]: ((Z=Y|~host(Z)=host(Y))|(~setIn(Y,alive)|~setIn(Z,alive)))))&(![Y,Z]: ((~setIn(Z,alive)|~elem(m_Ack(Z,Y),queue(host(Z))))|leq(host(Y),index(pendack,host(Z))))))&(![Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|(![Y]: ~elem(m_Ack(Y,Z),queue(host(Y)))))))&(![Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|(![Y]: ~elem(m_Ack(Z,Y),queue(host(Z)))))))&(![Y]: (((~index(status,host(Y))=elec_1&~index(status,host(Y))=elec_2)|~setIn(Y,alive))|index(elid,host(Y))=Y)))&(![Pid0]: ((![Y]: ((![Z]: (~elem(m_Down(Y),queue(host(Z)))|~elem(m_Ack(Pid0,Z),queue(host(Pid0)))))|~host(Pid0)=host(Y)))|~setIn(Pid0,alive))))&(![Z,Pid0]: ((![Y]: (((~setIn(Z,alive)|~setIn(Pid0,alive))|~elem(m_Ack(Pid0,Y),queue(host(Pid0))))|~host(Z)=host(Y)))|~setIn(host(Pid0),index(down,host(Z))))))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|~leq(index(pendack,host(Y)),index(pendack,host(Z))))))&(![Y]: ((![Pid0]: (((leq(index(pendack,host(Pid0)),host(Y))|~setIn(Pid0,alive))|(![Z]: ~elem(m_Halt(Pid0),queue(host(Z)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&((![Z,Pid0]: ((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Z)=index(pendack,host(Pid0))))|(![Y]: ((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&queue(host(sK4_skl))=cons(m_Halt(sK5_skl),sK6_skl))&(setIn(sK4_skl,alive)&(~host(sK4_skl)=host(sK7_skl)&(host(sK5_skl)=host(sK8_skl)&(~host(sK4_skl)=host(sK8_skl)&(((((setIn(sK8_skl,alive)&leq(nbr_proc,index(pendack,host(sK8_skl))))&elem(m_Ack(sK8_skl,sK9_skl),snoc(queue(host(sK8_skl)),m_Ack(sK5_skl,sK4_skl))))&index(status,host(sK8_skl))=elec_2)&host(sK9_skl)=index(pendack,host(sK8_skl)))&((setIn(sK7_skl,alive)&index(ldr,host(sK7_skl))=host(sK7_skl))&index(status,host(sK7_skl))=norm)))))))),
% 7.16/1.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(W,sK4_skl),skolemize(X,sK5_skl),skolemize(V,sK6_skl),skolemize(Y,sK7_skl),skolemize(X0,sK8_skl),skolemize(Z,sK9_skl)],[f213])).
% 7.16/1.50 fof(f229,plain,(
% 7.16/1.50 ![X0,X1,X2]: (leq(index(pendack,host(X0)),host(X1))|~setIn(X0,alive)|~elem(m_Halt(X0),queue(host(X2)))|~index(status,host(X0))=elec_2|~setIn(X1,alive)|~index(ldr,host(X1))=host(X1)|~index(status,host(X1))=norm)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f230,plain,(
% 7.16/1.50 ![X0,X1,X2]: (~setIn(X0,alive)|~elem(m_Ack(X0,X1),queue(host(X0)))|~leq(nbr_proc,index(pendack,host(X0)))|~index(status,host(X0))=elec_2|~host(X1)=index(pendack,host(X0))|~setIn(X2,alive)|~index(ldr,host(X2))=host(X2)|~index(status,host(X2))=norm)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f231,plain,(
% 7.16/1.50 queue(host(sK4_skl))=cons(m_Halt(sK5_skl),sK6_skl)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f233,plain,(
% 7.16/1.50 ~host(sK4_skl)=host(sK7_skl)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f234,plain,(
% 7.16/1.50 host(sK5_skl)=host(sK8_skl)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f236,plain,(
% 7.16/1.50 setIn(sK8_skl,alive)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f237,plain,(
% 7.16/1.50 leq(nbr_proc,index(pendack,host(sK8_skl)))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f238,plain,(
% 7.16/1.50 elem(m_Ack(sK8_skl,sK9_skl),snoc(queue(host(sK8_skl)),m_Ack(sK5_skl,sK4_skl)))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f239,plain,(
% 7.16/1.50 index(status,host(sK8_skl))=elec_2),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f240,plain,(
% 7.16/1.50 host(sK9_skl)=index(pendack,host(sK8_skl))),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f241,plain,(
% 7.16/1.50 setIn(sK7_skl,alive)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f242,plain,(
% 7.16/1.50 index(ldr,host(sK7_skl))=host(sK7_skl)),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f243,plain,(
% 7.16/1.50 index(status,host(sK7_skl))=norm),
% 7.16/1.50 inference(cnf_transformation,[status(thm)],[f214])).
% 7.16/1.50 fof(f244,definition,(
% 7.16/1.50 ![X0,X1]: (sQ0_spl <=> (~setIn(X0,alive)|~elem(m_Ack(X0,X1),queue(host(X0)))|~leq(nbr_proc,index(pendack,host(X0)))|~index(status,host(X0))=elec_2|~host(X1)=index(pendack,host(X0))))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f245,plain,(
% 7.16/1.50 ![X0,X1]: (~setIn(X0,alive)|~elem(m_Ack(X0,X1),queue(host(X0)))|~leq(nbr_proc,index(pendack,host(X0)))|~index(status,host(X0))=elec_2|~host(X1)=index(pendack,host(X0))|~sQ0_spl)),
% 7.16/1.50 inference(component_clause,[status(thm)],[f244])).
% 7.16/1.50 fof(f247,definition,(
% 7.16/1.50 ![X2]: (sQ1_spl <=> (~setIn(X2,alive)|~index(ldr,host(X2))=host(X2)|~index(status,host(X2))=norm))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f248,plain,(
% 7.16/1.50 ![X0]: (~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ1_spl)),
% 7.16/1.50 inference(component_clause,[status(thm)],[f247])).
% 7.16/1.50 fof(f250,plain,(
% 7.16/1.50 sQ0_spl|sQ1_spl),
% 7.16/1.50 inference(split_clause,[status(thm)],[f230,f244,f247])).
% 7.16/1.50 fof(f251,plain,(
% 7.16/1.50 ![X0,X1]: (elem(X0,cons(X0,X1)))),
% 7.16/1.50 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 7.16/1.50 fof(f260,plain,(
% 7.16/1.50 leq(nbr_proc,index(pendack,host(sK5_skl)))),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f234,f237])).
% 7.16/1.50 fof(f261,plain,(
% 7.16/1.50 elem(m_Ack(sK8_skl,sK9_skl),snoc(queue(host(sK5_skl)),m_Ack(sK5_skl,sK4_skl)))),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f234,f238])).
% 7.16/1.50 fof(f262,plain,(
% 7.16/1.50 index(status,host(sK5_skl))=elec_2),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f234,f239])).
% 7.16/1.50 fof(f263,plain,(
% 7.16/1.50 leq(nbr_proc,host(sK9_skl))),
% 7.16/1.50 inference(backward_demodulation,[status(thm)],[f264,f260])).
% 7.16/1.50 fof(f264,plain,(
% 7.16/1.50 host(sK9_skl)=index(pendack,host(sK5_skl))),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f234,f240])).
% 7.16/1.50 fof(f356,definition,(
% 7.16/1.50 sQ17_spl <=> (setIn(sK8_skl,alive))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f358,plain,(
% 7.16/1.50 ~setIn(sK8_skl,alive)|sQ17_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f356])).
% 7.16/1.50 fof(f363,plain,(
% 7.16/1.50 $false|sQ17_spl),
% 7.16/1.50 inference(forward_subsumption_resolution,[status(thm)],[f358,f236])).
% 7.16/1.50 fof(f364,plain,(
% 7.16/1.50 sQ17_spl),
% 7.16/1.50 inference(contradiction_clause,[status(thm)],[f363])).
% 7.16/1.50 fof(f488,plain,(
% 7.16/1.50 ~leq(host(sK9_skl),nbr_proc)|nbr_proc=host(sK9_skl)),
% 7.16/1.50 inference(resolution,[status(thm)],[f196,f263])).
% 7.16/1.50 fof(f509,definition,(
% 7.16/1.50 sQ26_spl <=> (leq(host(sK9_skl),nbr_proc))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f511,plain,(
% 7.16/1.50 ~leq(host(sK9_skl),nbr_proc)|sQ26_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f509])).
% 7.16/1.50 fof(f512,definition,(
% 7.16/1.50 sQ27_spl <=> (nbr_proc=host(sK9_skl))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f513,plain,(
% 7.16/1.50 nbr_proc=host(sK9_skl)|~sQ27_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f512])).
% 7.16/1.50 fof(f515,plain,(
% 7.16/1.50 ~sQ26_spl|sQ27_spl),
% 7.16/1.50 inference(split_clause,[status(thm)],[f488,f509,f512])).
% 7.16/1.50 fof(f525,plain,(
% 7.16/1.50 $false|sQ26_spl),
% 7.16/1.50 inference(forward_subsumption_resolution,[status(thm)],[f511,f76])).
% 7.16/1.50 fof(f526,plain,(
% 7.16/1.50 sQ26_spl),
% 7.16/1.50 inference(contradiction_clause,[status(thm)],[f525])).
% 7.16/1.50 fof(f534,plain,(
% 7.16/1.50 nbr_proc=index(pendack,host(sK5_skl))|~sQ27_spl),
% 7.16/1.50 inference(backward_demodulation,[status(thm)],[f513,f264])).
% 7.16/1.50 fof(f671,definition,(
% 7.16/1.50 sQ44_spl <=> (index(status,host(sK8_skl))=elec_2)),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f673,plain,(
% 7.16/1.50 ~index(status,host(sK8_skl))=elec_2|sQ44_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f671])).
% 7.16/1.50 fof(f793,definition,(
% 7.16/1.50 sQ55_spl <=> (setIn(sK5_skl,alive))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f795,plain,(
% 7.16/1.50 ~setIn(sK5_skl,alive)|sQ55_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f793])).
% 7.16/1.50 fof(f796,definition,(
% 7.16/1.50 sQ56_spl <=> (index(status,host(sK5_skl))=elec_2)),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f798,plain,(
% 7.16/1.50 ~index(status,host(sK5_skl))=elec_2|sQ56_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f796])).
% 7.16/1.50 fof(f823,plain,(
% 7.16/1.50 ~index(status,host(sK5_skl))=elec_2|sQ44_spl),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f234,f673])).
% 7.16/1.50 fof(f824,plain,(
% 7.16/1.50 ~elec_2=elec_2|sQ44_spl),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f262,f823])).
% 7.16/1.50 fof(f825,plain,(
% 7.16/1.50 $false|sQ44_spl),
% 7.16/1.50 inference(trivial_equality_resolution,[status(thm)],[f824])).
% 7.16/1.50 fof(f826,plain,(
% 7.16/1.50 sQ44_spl),
% 7.16/1.50 inference(contradiction_clause,[status(thm)],[f825])).
% 7.16/1.50 fof(f828,plain,(
% 7.16/1.50 ~elec_2=elec_2|sQ56_spl),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f262,f798])).
% 7.16/1.50 fof(f829,plain,(
% 7.16/1.50 $false|sQ56_spl),
% 7.16/1.50 inference(trivial_equality_resolution,[status(thm)],[f828])).
% 7.16/1.50 fof(f830,plain,(
% 7.16/1.50 sQ56_spl),
% 7.16/1.50 inference(contradiction_clause,[status(thm)],[f829])).
% 7.16/1.50 fof(f852,plain,(
% 7.16/1.50 ![X0,X1]: (leq(index(pendack,host(X0)),host(sK7_skl))|~setIn(X0,alive)|~elem(m_Halt(X0),queue(host(X1)))|~index(status,host(X0))=elec_2|~index(ldr,host(sK7_skl))=host(sK7_skl)|~index(status,host(sK7_skl))=norm)),
% 7.16/1.50 inference(resolution,[status(thm)],[f229,f241])).
% 7.16/1.50 fof(f867,definition,(
% 7.16/1.50 ![X0,X1]: (sQ68_spl <=> (leq(index(pendack,host(X0)),host(sK7_skl))|~setIn(X0,alive)|~elem(m_Halt(X0),queue(host(X1)))|~index(status,host(X0))=elec_2))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f868,plain,(
% 7.16/1.50 ![X0,X1]: (leq(index(pendack,host(X0)),host(sK7_skl))|~setIn(X0,alive)|~elem(m_Halt(X0),queue(host(X1)))|~index(status,host(X0))=elec_2|~sQ68_spl)),
% 7.16/1.50 inference(component_clause,[status(thm)],[f867])).
% 7.16/1.50 fof(f870,definition,(
% 7.16/1.50 sQ69_spl <=> (index(ldr,host(sK7_skl))=host(sK7_skl))),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f872,plain,(
% 7.16/1.50 ~index(ldr,host(sK7_skl))=host(sK7_skl)|sQ69_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f870])).
% 7.16/1.50 fof(f873,definition,(
% 7.16/1.50 sQ70_spl <=> (index(status,host(sK7_skl))=norm)),
% 7.16/1.50 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 7.16/1.50 fof(f875,plain,(
% 7.16/1.50 ~index(status,host(sK7_skl))=norm|sQ70_spl),
% 7.16/1.50 inference(component_clause,[status(thm)],[f873])).
% 7.16/1.50 fof(f876,plain,(
% 7.16/1.50 sQ68_spl|~sQ69_spl|~sQ70_spl),
% 7.16/1.50 inference(split_clause,[status(thm)],[f852,f867,f870,f873])).
% 7.16/1.50 fof(f904,plain,(
% 7.16/1.50 ~norm=norm|sQ70_spl),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f243,f875])).
% 7.16/1.50 fof(f905,plain,(
% 7.16/1.50 $false|sQ70_spl),
% 7.16/1.50 inference(trivial_equality_resolution,[status(thm)],[f904])).
% 7.16/1.50 fof(f906,plain,(
% 7.16/1.50 sQ70_spl),
% 7.16/1.50 inference(contradiction_clause,[status(thm)],[f905])).
% 7.16/1.50 fof(f907,plain,(
% 7.16/1.50 ~host(sK7_skl)=host(sK7_skl)|sQ69_spl),
% 7.16/1.50 inference(forward_demodulation,[status(thm)],[f242,f872])).
% 7.16/1.50 fof(f908,plain,(
% 7.16/1.50 $false|sQ69_spl),
% 7.16/1.50 inference(trivial_equality_resolution,[status(thm)],[f907])).
% 7.16/1.50 fof(f909,plain,(
% 7.16/1.50 sQ69_spl),
% 7.16/1.50 inference(contradiction_clause,[status(thm)],[f908])).
% 7.16/1.50 fof(f918,plain,(
% 7.16/1.50 elem(m_Halt(sK5_skl),queue(host(sK4_skl)))),
% 7.16/1.50 inference(paramodulation,[status(thm)],[f231,f251])).
% 7.16/1.50 fof(f1009,plain,(
% 7.16/1.50 m_Ack(sK8_skl,sK9_skl)=m_Ack(sK5_skl,sK4_skl)|elem(m_Ack(sK8_skl,sK9_skl),queue(host(sK5_skl)))),
% 7.16/1.50 inference(resolution,[status(thm)],[f261,f145])).
% 7.16/1.50 fof(f1014,definition,(
% 7.16/1.50 sQ90_spl <=> (m_Ack(sK8_skl,sK9_skl)=m_Ack(sK5_skl,sK4_skl))),
% 7.16/1.51 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 7.16/1.51 fof(f1015,plain,(
% 7.16/1.51 m_Ack(sK8_skl,sK9_skl)=m_Ack(sK5_skl,sK4_skl)|~sQ90_spl),
% 7.16/1.51 inference(component_clause,[status(thm)],[f1014])).
% 7.16/1.51 fof(f1017,definition,(
% 7.16/1.51 sQ91_spl <=> (elem(m_Ack(sK8_skl,sK9_skl),queue(host(sK5_skl))))),
% 7.16/1.51 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 7.16/1.51 fof(f1018,plain,(
% 7.16/1.51 elem(m_Ack(sK8_skl,sK9_skl),queue(host(sK5_skl)))|~sQ91_spl),
% 7.16/1.51 inference(component_clause,[status(thm)],[f1017])).
% 7.16/1.51 fof(f1020,plain,(
% 7.16/1.51 sQ90_spl|sQ91_spl),
% 7.16/1.51 inference(split_clause,[status(thm)],[f1009,f1014,f1017])).
% 7.16/1.51 fof(f1042,plain,(
% 7.16/1.51 ![X0]: (~setIn(sK8_skl,alive)|~elem(m_Ack(sK8_skl,X0),queue(host(sK5_skl)))|~leq(nbr_proc,index(pendack,host(sK8_skl)))|~index(status,host(sK8_skl))=elec_2|~host(X0)=index(pendack,host(sK8_skl))|~sQ0_spl)),
% 7.16/1.51 inference(paramodulation,[status(thm)],[f234,f245])).
% 7.16/1.51 fof(f1050,definition,(
% 7.16/1.51 ![X0]: (sQ97_spl <=> (~elem(m_Ack(sK8_skl,X0),queue(host(sK5_skl)))|~host(X0)=index(pendack,host(sK8_skl))))),
% 7.16/1.51 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 7.16/1.51 fof(f1051,plain,(
% 7.16/1.51 ![X0]: (~elem(m_Ack(sK8_skl,X0),queue(host(sK5_skl)))|~host(X0)=index(pendack,host(sK8_skl))|~sQ97_spl)),
% 7.16/1.51 inference(component_clause,[status(thm)],[f1050])).
% 7.16/1.51 fof(f1053,definition,(
% 7.16/1.51 sQ98_spl <=> (leq(nbr_proc,index(pendack,host(sK8_skl))))),
% 7.16/1.51 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 7.16/1.51 fof(f1055,plain,(
% 7.16/1.51 ~leq(nbr_proc,index(pendack,host(sK8_skl)))|sQ98_spl),
% 7.16/1.51 inference(component_clause,[status(thm)],[f1053])).
% 7.16/1.51 fof(f1056,plain,(
% 7.16/1.51 ~sQ17_spl|sQ97_spl|~sQ98_spl|~sQ44_spl|~sQ0_spl),
% 7.16/1.51 inference(split_clause,[status(thm)],[f1042,f356,f1050,f1053,f671,f244])).
% 7.16/1.51 fof(f1057,plain,(
% 7.16/1.51 ![X0]: (~elem(m_Ack(sK8_skl,X0),queue(host(sK5_skl)))|~host(X0)=index(pendack,host(sK5_skl))|~sQ97_spl)),
% 7.16/1.51 inference(forward_demodulation,[status(thm)],[f234,f1051])).
% 7.16/1.51 fof(f1058,plain,(
% 7.16/1.51 ![X0]: (~elem(m_Ack(sK8_skl,X0),queue(host(sK5_skl)))|~host(X0)=nbr_proc|~sQ27_spl|~sQ97_spl)),
% 7.16/1.51 inference(forward_demodulation,[status(thm)],[f534,f1057])).
% 7.16/1.51 fof(f1059,plain,(
% 7.16/1.51 ~leq(nbr_proc,index(pendack,host(sK5_skl)))|sQ98_spl),
% 7.16/1.51 inference(forward_demodulation,[status(thm)],[f234,f1055])).
% 7.16/1.51 fof(f1060,plain,(
% 7.16/1.51 ~leq(nbr_proc,nbr_proc)|~sQ27_spl|sQ98_spl),
% 7.16/1.51 inference(forward_demodulation,[status(thm)],[f534,f1059])).
% 7.16/1.51 fof(f1061,plain,(
% 7.16/1.51 $false|~sQ27_spl|sQ98_spl),
% 7.16/1.51 inference(forward_subsumption_resolution,[status(thm)],[f1060,f192])).
% 7.16/1.51 fof(f1062,plain,(
% 7.16/1.51 ~sQ27_spl|sQ98_spl),
% 7.16/1.51 inference(contradiction_clause,[status(thm)],[f1061])).
% 7.16/1.51 fof(f2016,plain,(
% 7.16/1.51 ~index(ldr,host(sK7_skl))=host(sK7_skl)|~index(status,host(sK7_skl))=norm|~sQ1_spl),
% 7.16/1.51 inference(resolution,[status(thm)],[f248,f241])).
% 7.16/1.51 fof(f2019,plain,(
% 7.16/1.51 ~sQ69_spl|~sQ70_spl|~sQ1_spl),
% 7.16/1.51 inference(split_clause,[status(thm)],[f2016,f870,f873,f247])).
% 7.16/1.51 fof(f2496,plain,(
% 7.16/1.51 sK9_skl=sK4_skl|~sQ90_spl),
% 7.16/1.51 inference(resolution,[status(thm)],[f1015,f123])).
% 7.16/1.51 fof(f2497,plain,(
% 7.16/1.51 sK8_skl=sK5_skl|~sQ90_spl),
% 7.16/1.51 inference(resolution,[status(thm)],[f1015,f120])).
% 7.16/1.51 fof(f2525,plain,(
% 7.16/1.51 setIn(sK5_skl,alive)|~sQ90_spl),
% 7.16/1.51 inference(backward_demodulation,[status(thm)],[f2497,f236])).
% 7.16/1.51 fof(f6400,plain,(
% 7.16/1.51 leq(index(pendack,host(sK5_skl)),host(sK7_skl))|~setIn(sK5_skl,alive)|~index(status,host(sK5_skl))=elec_2|~sQ68_spl),
% 7.16/1.51 inference(resolution,[status(thm)],[f918,f868])).
% 7.16/1.51 fof(f6406,definition,(
% 7.16/1.51 sQ269_spl <=> (leq(index(pendack,host(sK5_skl)),host(sK7_skl)))),
% 7.16/1.51 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 7.16/1.51 fof(f6407,plain,(
% 7.16/1.51 leq(index(pendack,host(sK5_skl)),host(sK7_skl))|~sQ269_spl),
% 7.16/1.51 inference(component_clause,[status(thm)],[f6406])).
% 7.16/1.51 fof(f6409,plain,(
% 7.16/1.51 sQ269_spl|~sQ55_spl|~sQ56_spl|~sQ68_spl),
% 7.16/1.51 inference(split_clause,[status(thm)],[f6400,f6406,f793,f796,f867])).
% 7.16/1.51 fof(f6422,plain,(
% 7.16/1.51 leq(nbr_proc,host(sK7_skl))|~sQ27_spl|~sQ269_spl),
% 7.16/1.51 inference(forward_demodulation,[status(thm)],[f534,f6407])).
% 7.16/1.51 fof(f7282,plain,(
% 7.16/1.51 ~leq(host(sK7_skl),nbr_proc)|host(sK7_skl)=nbr_proc|~sQ27_spl|~sQ269_spl),
% 7.16/1.51 inference(resolution,[status(thm)],[f6422,f196])).
% 7.16/1.51 fof(f7291,definition,(
% 7.16/1.51 sQ297_spl <=> (leq(host(sK7_skl),nbr_proc))),
% 7.16/1.51 introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition])).
% 7.16/1.51 fof(f7293,plain,(
% 7.16/1.51 ~leq(host(sK7_skl),nbr_proc)|sQ297_spl),
% 7.16/1.51 inference(component_clause,[status(thm)],[f7291])).
% 7.16/1.51 fof(f7294,definition,(
% 7.16/1.51 sQ298_spl <=> (host(sK7_skl)=nbr_proc)),
% 7.16/1.51 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 7.16/1.51 fof(f7297,plain,(
% 7.16/1.51 ~sQ297_spl|sQ298_spl|~sQ27_spl|~sQ269_spl),
% 7.16/1.51 inference(split_clause,[status(thm)],[f7282,f7291,f7294,f512,f6406])).
% 7.16/1.51 fof(f11910,plain,(
% 7.16/1.51 ~host(sK9_skl)=nbr_proc|~sQ91_spl|~sQ27_spl|~sQ97_spl),
% 7.16/1.51 inference(resolution,[status(thm)],[f1018,f1058])).
% 7.16/1.51 fof(f11921,plain,(
% 7.16/1.51 ~nbr_proc=nbr_proc|~sQ91_spl|~sQ27_spl|~sQ97_spl),
% 7.16/1.51 inference(forward_demodulation,[status(thm)],[f513,f11910])).
% 7.16/1.51 fof(f11922,plain,(
% 7.16/1.51 $false|~sQ91_spl|~sQ27_spl|~sQ97_spl),
% 7.16/1.51 inference(trivial_equality_resolution,[status(thm)],[f11921])).
% 7.16/1.51 fof(f11923,plain,(
% 7.16/1.51 ~sQ91_spl|~sQ27_spl|~sQ97_spl),
% 7.16/1.51 inference(contradiction_clause,[status(thm)],[f11922])).
% 7.16/1.51 fof(f12048,plain,(
% 7.16/1.51 $false|sQ55_spl|~sQ90_spl),
% 7.16/1.51 inference(forward_subsumption_resolution,[status(thm)],[f2525,f795])).
% 7.16/1.51 fof(f12049,plain,(
% 7.16/1.51 sQ55_spl|~sQ90_spl),
% 7.16/1.51 inference(contradiction_clause,[status(thm)],[f12048])).
% 7.16/1.51 fof(f12096,plain,(
% 7.16/1.51 ~nbr_proc=host(sK7_skl)|~sQ90_spl|~sQ27_spl),
% 7.16/1.51 inference(backward_demodulation,[status(thm)],[f12112,f233])).
% 7.16/1.51 fof(f12112,plain,(
% 7.16/1.51 nbr_proc=host(sK4_skl)|~sQ90_spl|~sQ27_spl),
% 7.16/1.51 inference(forward_demodulation,[status(thm)],[f2496,f513])).
% 7.16/1.51 fof(f12173,plain,(
% 7.16/1.51 $false|sQ297_spl),
% 7.16/1.51 inference(forward_subsumption_resolution,[status(thm)],[f7293,f76])).
% 7.16/1.51 fof(f12174,plain,(
% 7.16/1.51 sQ297_spl),
% 7.16/1.51 inference(contradiction_clause,[status(thm)],[f12173])).
% 7.16/1.51 fof(f12179,plain,(
% 7.16/1.51 ~sQ298_spl|~sQ90_spl|~sQ27_spl),
% 7.16/1.51 inference(split_clause,[status(thm)],[f12096,f7294,f1014,f512])).
% 7.16/1.51 fof(f12184,plain,(
% 7.16/1.51 $false),
% 7.16/1.51 inference(sat_refutation,[status(thm)],[f250,f364,f515,f526,f826,f830,f876,f906,f909,f1020,f1056,f1062,f2019,f6409,f7297,f11923,f12049,f12174,f12179])).
% 7.16/1.51 % SZS output end CNFRefutation for theBenchmark.p
% 7.16/1.55 % Elapsed time: 1.173240 seconds
% 7.16/1.55 % CPU time: 8.923834 seconds
% 7.16/1.55 % Total memory used: 169.135 MB
% 7.16/1.55 % Net memory used: 157.647 MB
%------------------------------------------------------------------------------