%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV473+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:54 PM UTC 2026
% Result : Theorem 101.98s 13.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV473+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:51:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 101.98/13.42 % Refutation found
% 101.98/13.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 101.98/13.42 % SZS output start CNFRefutation for theBenchmark
% 101.98/13.42 fof(f3,axiom,(
% 101.98/13.42 (! [P] : leq(s(zero),host(P)) )),
% 101.98/13.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.98/13.42 fof(f5,axiom,(
% 101.98/13.42 (! [P] : leq(host(P),nbr_proc) )),
% 101.98/13.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.98/13.42 fof(f47,axiom,(
% 101.98/13.42 (! [X,Y,Q] :( elem(X,cons(Y,Q))<=> ( X = Y| elem(X,Q) ) ) )),
% 101.98/13.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.98/13.42 fof(f62,axiom,(
% 101.98/13.42 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 101.98/13.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.98/13.42 fof(f67,conjecture,(
% 101.98/13.42 (! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( elem(m_Down(Pid0),queue(host(Z)))=> host(Pid0) != host(Z) ))& (! [Z,Pid0] :( host(Pid0) = nbr_proc=> ~ elem(m_NotNorm(Z),queue(host(Pid0))) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& host(Pid0) = host(Z)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid20) )=> ~ elem(m_Down(Z),queue(host(Pid20))) ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& host(Pid0) = host(Z)& index(status,host(Pid0)) = wait& host(index(elid,host(Pid0))) = host(Pid20) )=> ~ elem(m_Down(Z),queue(host(Pid20))) ))& (! [Z,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& elem(m_Down(Pid30),queue(host(Pid20))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& setIn(host(Pid30),index(down,host(Pid20))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid0) = nbr_proc& host(Pid0) = host(Pid30)& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid30),queue(host(Z))) ) ))& queue(host(X)) = cons(m_Ack(W,Y),V) )=> ( setIn(X,alive)=> ( ~ ( index(elid,host(X)) = W& index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> (! [Z] :( host(X) != host(Z)=> (! [W0,X0,Y0] :( host(X) = host(Y0)=> ( ( (! [V0] :( ( ~ leq(host(Y0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Y0)))| V0 = host(X0) ) ))& elem(m_Down(X0),V)& host(Y0) = host(W0)& host(Y0) = nbr_proc& index(status,host(Y0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(W0),queue(host(Z))) ) ) ) )) )) ) ) )),
% 101.98/13.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 101.98/13.42 fof(f68,negated_conjecture,(
% 101.98/13.42 ~((! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( elem(m_Down(Pid0),queue(host(Z)))=> host(Pid0) != host(Z) ))& (! [Z,Pid0] :( host(Pid0) = nbr_proc=> ~ elem(m_NotNorm(Z),queue(host(Pid0))) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& host(Pid0) = host(Z)& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid20) )=> ~ elem(m_Down(Z),queue(host(Pid20))) ))& (! [Z,Pid20,Pid0] :( ( host(Pid0) != host(Pid20)& setIn(Pid0,alive)& host(Pid0) = host(Z)& index(status,host(Pid0)) = wait& host(index(elid,host(Pid0))) = host(Pid20) )=> ~ elem(m_Down(Z),queue(host(Pid20))) ))& (! [Z,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& elem(m_Down(Pid30),queue(host(Pid20))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( host(Pid20) != host(Z)& setIn(Z,alive)& setIn(Pid20,alive)& host(Pid30) = host(Z)& host(Pid0) = host(Pid20) )=> ~ ( elem(m_Down(Pid0),queue(host(Z)))& setIn(host(Pid30),index(down,host(Pid20))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid0) = nbr_proc& host(Pid0) = host(Pid30)& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid30),queue(host(Z))) ) ))& queue(host(X)) = cons(m_Ack(W,Y),V) )=> ( setIn(X,alive)=> ( ~ ( index(elid,host(X)) = W& index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> (! [Z] :( host(X) != host(Z)=> (! [W0,X0,Y0] :( host(X) = host(Y0)=> ( ( (! [V0] :( ( ~ leq(host(Y0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Y0)))| V0 = host(X0) ) ))& elem(m_Down(X0),V)& host(Y0) = host(W0)& host(Y0) = nbr_proc& index(status,host(Y0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(W0),queue(host(Z))) ) ) ) )) )) ) ) ))),
% 101.98/13.42 inference(negated_conjecture,[status(cth)],[f67])).
% 101.98/13.42 fof(f74,plain,(
% 101.98/13.42 ![X0]: (leq(s(zero),host(X0)))),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f3])).
% 101.98/13.42 fof(f76,plain,(
% 101.98/13.42 ![X0]: (leq(host(X0),nbr_proc))),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f5])).
% 101.98/13.42 fof(f138,plain,(
% 101.98/13.42 ![X,Y,Q]: ((~elem(X,cons(Y,Q))|(X=Y|elem(X,Q)))&(elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 101.98/13.42 inference(NNF_transformation,[status(thm)],[f47])).
% 101.98/13.42 fof(f139,plain,(
% 101.98/13.42 (![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))))),
% 101.98/13.42 inference(miniscoping,[status(thm)],[f138])).
% 101.98/13.42 fof(f142,plain,(
% 101.98/13.42 ![X0,X1,X2]: (elem(X0,cons(X1,X2))|~elem(X0,X2))),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f139])).
% 101.98/13.42 fof(f194,plain,(
% 101.98/13.42 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 101.98/13.42 inference(NNF_transformation,[status(thm)],[f62])).
% 101.98/13.42 fof(f195,plain,(
% 101.98/13.42 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 101.98/13.42 inference(miniscoping,[status(thm)],[f194])).
% 101.98/13.42 fof(f196,plain,(
% 101.98/13.42 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f195])).
% 101.98/13.42 fof(f212,plain,(
% 101.98/13.42 (?[V,W,X,Y]: ((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Z,Pid0]: (~host(Pid0)=nbr_proc|~elem(m_NotNorm(Z),queue(host(Pid0))))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid20,Pid0]: (((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid20))|~elem(m_Down(Z),queue(host(Pid20))))))&(![Z,Pid20,Pid0]: (((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Pid0))=wait)|~host(index(elid,host(Pid0)))=host(Pid20))|~elem(m_Down(Z),queue(host(Pid20))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~elem(m_Down(Pid30),queue(host(Pid20)))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~setIn(host(Pid30),index(down,host(Pid20)))))))&(![Z,Pid30,Pid20,Pid0]: ((((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1)|(~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z)))))))&queue(host(X))=cons(m_Ack(W,Y),V))&(setIn(X,alive)&(((~index(elid,host(X))=W|~index(status,host(X))=elec_2)|~host(Y)=index(pendack,host(X)))&(?[Z]: (~host(X)=host(Z)&(?[W0,X0,Y0]: (host(X)=host(Y0)&((((((![V0]: ((leq(host(Y0),V0)|~leq(s(zero),V0))|(setIn(V0,index(down,host(Y0)))|V0=host(X0))))&elem(m_Down(X0),V))&host(Y0)=host(W0))&host(Y0)=nbr_proc)&index(status,host(Y0))=elec_1)&(setIn(Z,alive)&elem(m_Down(W0),queue(host(Z)))))))))))))),
% 101.98/13.42 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 101.98/13.42 fof(f213,plain,(
% 101.98/13.42 ?[V,W,X,Y]: ((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Pid0]: (~host(Pid0)=nbr_proc|(![Z]: ~elem(m_NotNorm(Z),queue(host(Pid0)))))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid20]: ((![Pid0]: ((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid20)))|~elem(m_Down(Z),queue(host(Pid20))))))&(![Z,Pid20]: ((![Pid0]: ((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Pid0))=wait)|~host(index(elid,host(Pid0)))=host(Pid20)))|~elem(m_Down(Z),queue(host(Pid20))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~elem(m_Down(Pid30),queue(host(Pid20)))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~setIn(host(Pid30),index(down,host(Pid20)))))))&(![Pid30]: ((![Pid0]: ((((![Pid20]: ((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z))))))))&queue(host(X))=cons(m_Ack(W,Y),V))&(setIn(X,alive)&(((~index(elid,host(X))=W|~index(status,host(X))=elec_2)|~host(Y)=index(pendack,host(X)))&(?[Z]: (~host(X)=host(Z)&(?[Y0]: (host(X)=host(Y0)&(?[W0]: (((((?[X0]: ((![V0]: ((leq(host(Y0),V0)|~leq(s(zero),V0))|(setIn(V0,index(down,host(Y0)))|V0=host(X0))))&elem(m_Down(X0),V)))&host(Y0)=host(W0))&host(Y0)=nbr_proc)&index(status,host(Y0))=elec_1)&(setIn(Z,alive)&elem(m_Down(W0),queue(host(Z)))))))))))))),
% 101.98/13.42 inference(miniscoping,[status(thm)],[f212])).
% 101.98/13.42 fof(f214,plain,(
% 101.98/13.42 ((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Pid0]: (~host(Pid0)=nbr_proc|(![Z]: ~elem(m_NotNorm(Z),queue(host(Pid0)))))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid20]: ((![Pid0]: ((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid20)))|~elem(m_Down(Z),queue(host(Pid20))))))&(![Z,Pid20]: ((![Pid0]: ((((host(Pid0)=host(Pid20)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Pid0))=wait)|~host(index(elid,host(Pid0)))=host(Pid20)))|~elem(m_Down(Z),queue(host(Pid20))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~elem(m_Down(Pid30),queue(host(Pid20)))))))&(![Z,Pid30,Pid20,Pid0]: (((((host(Pid20)=host(Z)|~setIn(Z,alive))|~setIn(Pid20,alive))|~host(Pid30)=host(Z))|~host(Pid0)=host(Pid20))|(~elem(m_Down(Pid0),queue(host(Z)))|~setIn(host(Pid30),index(down,host(Pid20)))))))&(![Pid30]: ((![Pid0]: ((((![Pid20]: (((~leq(host(Pid0),sK8_skl(Pid20,Pid0,Pid30))&leq(s(zero),sK8_skl(Pid20,Pid0,Pid30)))&(~setIn(sK8_skl(Pid20,Pid0,Pid30),index(down,host(Pid0)))&~sK8_skl(Pid20,Pid0,Pid30)=host(Pid20)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z))))))))&queue(host(sK6_skl))=cons(m_Ack(sK5_skl,sK7_skl),sK4_skl))&(setIn(sK6_skl,alive)&(((~index(elid,host(sK6_skl))=sK5_skl|~index(status,host(sK6_skl))=elec_2)|~host(sK7_skl)=index(pendack,host(sK6_skl)))&(~host(sK6_skl)=host(sK9_skl)&(host(sK6_skl)=host(sK10_skl)&((((((![V0]: ((leq(host(sK10_skl),V0)|~leq(s(zero),V0))|(setIn(V0,index(down,host(sK10_skl)))|V0=host(sK12_skl))))&elem(m_Down(sK12_skl),sK4_skl))&host(sK10_skl)=host(sK11_skl))&host(sK10_skl)=nbr_proc)&index(status,host(sK10_skl))=elec_1)&(setIn(sK9_skl,alive)&elem(m_Down(sK11_skl),queue(host(sK9_skl))))))))))),
% 101.98/13.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(V,sK4_skl),skolemize(W,sK5_skl),skolemize(X,sK6_skl),skolemize(Y,sK7_skl),skolemize(V0,sK8_skl(Pid20,Pid0,Pid30)),skolemize(Z,sK9_skl),skolemize(Y0,sK10_skl),skolemize(W0,sK11_skl),skolemize(X0,sK12_skl)],[f213])).
% 101.98/13.42 fof(f223,plain,(
% 101.98/13.42 ![X0,X1,X2,X3]: (host(X0)=host(X1)|~setIn(X1,alive)|~setIn(X0,alive)|~host(X2)=host(X1)|~host(X3)=host(X0)|~elem(m_Down(X3),queue(host(X1)))|~elem(m_Down(X2),queue(host(X0))))),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f224,plain,(
% 101.98/13.42 ![X0,X1,X2,X3]: (host(X0)=host(X1)|~setIn(X1,alive)|~setIn(X0,alive)|~host(X2)=host(X1)|~host(X3)=host(X0)|~elem(m_Down(X3),queue(host(X1)))|~setIn(host(X2),index(down,host(X0))))),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f229,plain,(
% 101.98/13.42 queue(host(sK6_skl))=cons(m_Ack(sK5_skl,sK7_skl),sK4_skl)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f230,plain,(
% 101.98/13.42 setIn(sK6_skl,alive)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f232,plain,(
% 101.98/13.42 ~host(sK6_skl)=host(sK9_skl)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f233,plain,(
% 101.98/13.42 host(sK6_skl)=host(sK10_skl)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f234,plain,(
% 101.98/13.42 ![X0]: (leq(host(sK10_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK10_skl)))|X0=host(sK12_skl))),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f235,plain,(
% 101.98/13.42 elem(m_Down(sK12_skl),sK4_skl)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f236,plain,(
% 101.98/13.42 host(sK10_skl)=host(sK11_skl)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f237,plain,(
% 101.98/13.42 host(sK10_skl)=nbr_proc),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f239,plain,(
% 101.98/13.42 setIn(sK9_skl,alive)),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f240,plain,(
% 101.98/13.42 elem(m_Down(sK11_skl),queue(host(sK9_skl)))),
% 101.98/13.42 inference(cnf_transformation,[status(thm)],[f214])).
% 101.98/13.42 fof(f341,plain,(
% 101.98/13.42 ![X0]: (~leq(nbr_proc,host(X0))|host(X0)=nbr_proc)),
% 101.98/13.42 inference(resolution,[status(thm)],[f196,f76])).
% 101.98/13.42 fof(f428,plain,(
% 101.98/13.42 ~nbr_proc=host(sK9_skl)),
% 101.98/13.42 inference(backward_demodulation,[status(thm)],[f429,f232])).
% 101.98/13.42 fof(f429,plain,(
% 101.98/13.42 host(sK6_skl)=nbr_proc),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f237,f233])).
% 101.98/13.42 fof(f430,plain,(
% 101.98/13.42 ![X0,X1,X2]: (host(sK6_skl)=host(X0)|~setIn(X0,alive)|~setIn(sK6_skl,alive)|~host(X1)=host(X0)|~host(X2)=host(sK6_skl)|~elem(m_Down(X2),queue(host(X0)))|~setIn(host(X1),index(down,nbr_proc)))),
% 101.98/13.42 inference(paramodulation,[status(thm)],[f429,f224])).
% 101.98/13.42 fof(f433,plain,(
% 101.98/13.42 ![X0,X1,X2]: (host(sK6_skl)=host(X0)|~setIn(X0,alive)|~setIn(sK6_skl,alive)|~host(X1)=host(X0)|~host(X2)=host(sK6_skl)|~elem(m_Down(X2),queue(host(X0)))|~elem(m_Down(X1),queue(nbr_proc)))),
% 101.98/13.42 inference(paramodulation,[status(thm)],[f429,f223])).
% 101.98/13.42 fof(f445,plain,(
% 101.98/13.42 ![X0,X1,X2]: (nbr_proc=host(X0)|~setIn(X0,alive)|~setIn(sK6_skl,alive)|~host(X1)=host(X0)|~host(X2)=host(sK6_skl)|~elem(m_Down(X2),queue(host(X0)))|~setIn(host(X1),index(down,nbr_proc)))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f429,f430])).
% 101.98/13.42 fof(f446,plain,(
% 101.98/13.42 ![X0,X1,X2]: (nbr_proc=host(X0)|~setIn(X0,alive)|~setIn(sK6_skl,alive)|~host(X1)=host(X0)|~host(X2)=nbr_proc|~elem(m_Down(X2),queue(host(X0)))|~setIn(host(X1),index(down,nbr_proc)))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f429,f445])).
% 101.98/13.42 fof(f447,plain,(
% 101.98/13.42 ![X0,X1,X2]: (nbr_proc=host(X0)|~setIn(X0,alive)|~host(X1)=host(X0)|~host(X2)=nbr_proc|~elem(m_Down(X2),queue(host(X0)))|~setIn(host(X1),index(down,nbr_proc)))),
% 101.98/13.42 inference(forward_subsumption_resolution,[status(thm)],[f446,f230])).
% 101.98/13.42 fof(f452,plain,(
% 101.98/13.42 ![X0,X1,X2]: (nbr_proc=host(X0)|~setIn(X0,alive)|~setIn(sK6_skl,alive)|~host(X1)=host(X0)|~host(X2)=host(sK6_skl)|~elem(m_Down(X2),queue(host(X0)))|~elem(m_Down(X1),queue(nbr_proc)))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f429,f433])).
% 101.98/13.42 fof(f453,plain,(
% 101.98/13.42 ![X0,X1,X2]: (nbr_proc=host(X0)|~setIn(X0,alive)|~setIn(sK6_skl,alive)|~host(X1)=host(X0)|~host(X2)=nbr_proc|~elem(m_Down(X2),queue(host(X0)))|~elem(m_Down(X1),queue(nbr_proc)))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f429,f452])).
% 101.98/13.42 fof(f454,plain,(
% 101.98/13.42 ![X0,X1,X2]: (nbr_proc=host(X0)|~setIn(X0,alive)|~host(X1)=host(X0)|~host(X2)=nbr_proc|~elem(m_Down(X2),queue(host(X0)))|~elem(m_Down(X1),queue(nbr_proc)))),
% 101.98/13.42 inference(forward_subsumption_resolution,[status(thm)],[f453,f230])).
% 101.98/13.42 fof(f500,plain,(
% 101.98/13.42 ![X0]: (elem(m_Down(sK12_skl),cons(X0,sK4_skl)))),
% 101.98/13.42 inference(resolution,[status(thm)],[f235,f142])).
% 101.98/13.42 fof(f554,plain,(
% 101.98/13.42 nbr_proc=host(sK11_skl)),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f237,f236])).
% 101.98/13.42 fof(f660,plain,(
% 101.98/13.42 queue(nbr_proc)=cons(m_Ack(sK5_skl,sK7_skl),sK4_skl)),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f429,f229])).
% 101.98/13.42 fof(f672,plain,(
% 101.98/13.42 ![X0]: (leq(nbr_proc,X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK10_skl)))|X0=host(sK12_skl))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f237,f234])).
% 101.98/13.42 fof(f673,plain,(
% 101.98/13.42 ![X0]: (leq(nbr_proc,X0)|~leq(s(zero),X0)|setIn(X0,index(down,nbr_proc))|X0=host(sK12_skl))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f237,f672])).
% 101.98/13.42 fof(f675,plain,(
% 101.98/13.42 ![X0]: (leq(nbr_proc,host(X0))|setIn(host(X0),index(down,nbr_proc))|host(X0)=host(sK12_skl))),
% 101.98/13.42 inference(resolution,[status(thm)],[f673,f74])).
% 101.98/13.42 fof(f1045,plain,(
% 101.98/13.42 ![X0]: (nbr_proc=host(sK9_skl)|~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~host(sK11_skl)=nbr_proc|~setIn(host(X0),index(down,nbr_proc)))),
% 101.98/13.42 inference(resolution,[status(thm)],[f447,f240])).
% 101.98/13.42 fof(f1052,plain,(
% 101.98/13.42 ![X0]: (nbr_proc=host(sK9_skl)|~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~nbr_proc=nbr_proc|~setIn(host(X0),index(down,nbr_proc)))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f554,f1045])).
% 101.98/13.42 fof(f1053,plain,(
% 101.98/13.42 ![X0]: (nbr_proc=host(sK9_skl)|~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~setIn(host(X0),index(down,nbr_proc)))),
% 101.98/13.42 inference(trivial_equality_resolution,[status(thm)],[f1052])).
% 101.98/13.42 fof(f1054,plain,(
% 101.98/13.42 ![X0]: (~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~setIn(host(X0),index(down,nbr_proc)))),
% 101.98/13.42 inference(forward_subsumption_resolution,[status(thm)],[f1053,f428])).
% 101.98/13.42 fof(f1149,plain,(
% 101.98/13.42 elem(m_Down(sK12_skl),queue(nbr_proc))),
% 101.98/13.42 inference(paramodulation,[status(thm)],[f660,f500])).
% 101.98/13.42 fof(f1280,plain,(
% 101.98/13.42 ![X0]: (nbr_proc=host(sK9_skl)|~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~host(sK11_skl)=nbr_proc|~elem(m_Down(X0),queue(nbr_proc)))),
% 101.98/13.42 inference(resolution,[status(thm)],[f454,f240])).
% 101.98/13.42 fof(f1285,plain,(
% 101.98/13.42 ![X0]: (nbr_proc=host(sK9_skl)|~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~nbr_proc=nbr_proc|~elem(m_Down(X0),queue(nbr_proc)))),
% 101.98/13.42 inference(forward_demodulation,[status(thm)],[f554,f1280])).
% 101.98/13.42 fof(f1286,plain,(
% 101.98/13.42 ![X0]: (nbr_proc=host(sK9_skl)|~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~elem(m_Down(X0),queue(nbr_proc)))),
% 101.98/13.42 inference(trivial_equality_resolution,[status(thm)],[f1285])).
% 101.98/13.42 fof(f1287,plain,(
% 101.98/13.42 ![X0]: (~setIn(sK9_skl,alive)|~host(X0)=host(sK9_skl)|~elem(m_Down(X0),queue(nbr_proc)))),
% 101.98/13.42 inference(forward_subsumption_resolution,[status(thm)],[f1286,f428])).
% 101.98/13.42 fof(f4303,plain,(
% 101.98/13.42 ![X0]: (~host(X0)=host(sK9_skl)|~setIn(host(X0),index(down,nbr_proc)))),
% 101.98/13.42 inference(forward_subsumption_resolution,[status(thm)],[f1054,f239])).
% 101.98/13.42 fof(f4304,plain,(
% 101.98/13.42 ![X0]: (~host(X0)=host(sK9_skl)|leq(nbr_proc,host(X0))|host(X0)=host(sK12_skl))),
% 101.98/13.42 inference(resolution,[status(thm)],[f4303,f675])).
% 101.98/13.42 fof(f4642,plain,(
% 101.98/13.42 ![X0]: (~host(X0)=host(sK9_skl)|~elem(m_Down(X0),queue(nbr_proc)))),
% 101.98/13.42 inference(forward_subsumption_resolution,[status(thm)],[f1287,f239])).
% 101.98/13.42 fof(f4643,plain,(
% 101.98/13.42 ~host(sK12_skl)=host(sK9_skl)),
% 101.98/13.42 inference(resolution,[status(thm)],[f4642,f1149])).
% 101.98/13.42 fof(f46954,plain,(
% 101.98/13.42 leq(nbr_proc,host(sK9_skl))|host(sK9_skl)=host(sK12_skl)),
% 101.98/13.47 inference(equality_resolution,[status(thm)],[f4304])).
% 101.98/13.47 fof(f46959,plain,(
% 101.98/13.47 leq(nbr_proc,host(sK9_skl))),
% 101.98/13.47 inference(forward_subsumption_resolution,[status(thm)],[f46954,f4643])).
% 101.98/13.47 fof(f47114,plain,(
% 101.98/13.47 host(sK9_skl)=nbr_proc),
% 101.98/13.47 inference(resolution,[status(thm)],[f46959,f341])).
% 101.98/13.47 fof(f47140,plain,(
% 101.98/13.47 $false),
% 101.98/13.47 inference(forward_subsumption_resolution,[status(thm)],[f47114,f428])).
% 101.98/13.47 % SZS output end CNFRefutation for theBenchmark.p
% 101.98/13.49 % Elapsed time: 13.113971 seconds
% 101.98/13.49 % CPU time: 103.280339 seconds
% 101.98/13.49 % Total memory used: 391.250 MB
% 101.98/13.49 % Net memory used: 339.283 MB
%------------------------------------------------------------------------------