%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV448+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 : n008.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:52 PM UTC 2026
% Result : Theorem 203.34s 26.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV448+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.76 % Computer : n008.cluster.edu
% 0.09/0.76 % Model : x86_64 x86_64
% 0.09/0.76 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.76 % Memory : 8046.5625MB
% 0.09/0.76 % OS : Linux 6.8.0-71-generic
% 0.09/0.76 % CPULimit : 300
% 0.09/0.76 % WCLimit : 300
% 0.09/0.76 % DateTime : Mon Sep 21 08:53:11 UTC 2026
% 0.09/0.76 % CPUTime :
% 0.09/0.78 % Drodi V4.1.1
% 203.34/26.57 % Refutation found
% 203.34/26.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 203.34/26.57 % SZS output start CNFRefutation for theBenchmark
% 203.34/26.57 fof(f2,axiom,(
% 203.34/26.57 (! [P,Q] :( s(host(P)) = host(Q)=> host(P) != host(Q) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f3,axiom,(
% 203.34/26.57 (! [P] : leq(s(zero),host(P)) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f4,axiom,(
% 203.34/26.57 leq(s(zero),nbr_proc) ),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f5,axiom,(
% 203.34/26.57 (! [P] : leq(host(P),nbr_proc) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f12,axiom,(
% 203.34/26.57 (! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f13,axiom,(
% 203.34/26.57 (! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f37,axiom,(
% 203.34/26.57 (! [X,Q] : tail(cons(X,Q)) = Q )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f42,axiom,(
% 203.34/26.57 (! [X,Q] : q_nil != cons(X,Q) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f43,axiom,(
% 203.34/26.57 (! [Y,Q] : q_nil != snoc(Q,Y) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f47,axiom,(
% 203.34/26.57 (! [X,Y,Q] :( elem(X,cons(Y,Q))<=> ( X = Y| elem(X,Q) ) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f49,axiom,(
% 203.34/26.57 (! [X] :( pidElem(X)<=> (? [Y] :( X = m_Halt(Y)| X = m_Down(Y) ) )) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f51,axiom,(
% 203.34/26.57 (! [X] : pidMsg(m_Down(X)) = X )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f53,axiom,(
% 203.34/26.57 (! [X] :( ordered(cons(X,q_nil))& ordered(snoc(q_nil,X)) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f59,axiom,(
% 203.34/26.57 (! [X] : ~ leq(s(X),X) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f60,axiom,(
% 203.34/26.57 (! [X] : leq(X,X) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f61,axiom,(
% 203.34/26.57 (! [X,Y] :( leq(X,Y)| leq(Y,X) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f62,axiom,(
% 203.34/26.57 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f63,axiom,(
% 203.34/26.57 (! [X,Y,Z] :( ( leq(X,Y)& leq(Y,Z) )=> leq(X,Z) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f64,axiom,(
% 203.34/26.57 (! [X,Y] :( leq(X,Y)<=> leq(s(X),s(Y)) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f65,axiom,(
% 203.34/26.57 (! [X,Y] :( leq(X,s(Y))<=> ( X = s(Y)| leq(X,Y) ) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f67,conjecture,(
% 203.34/26.57 (! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),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,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> Pid0 = Z ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& leq(nbr_proc,index(pendack,host(Pid0)))& index(status,host(Pid0)) = elec_2& host(Pid20) = index(pendack,host(Pid0)) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))& leq(nbr_proc,index(pendack,host(Pid0)))& index(status,host(Pid0)) = elec_2& host(Pid20) = index(pendack,host(Pid0)) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& ~ leq(host(Pid0),host(Z))& elem(m_Down(Pid20),queue(host(Pid0)))& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Down(Y),V) )=> ( setIn(X,alive)=> ( ~ leq(host(X),host(Y))=> ( ~ ( ( index(ldr,host(X)) = host(Y)& index(status,host(X)) = norm )| ( index(status,host(X)) = wait& host(Y) = host(index(elid,host(X))) ) )=> ( ( (! [Z] :( ( ~ leq(host(X),Z)& leq(s(zero),Z) )=> ( setIn(Z,index(down,host(X)))| Z = host(Y) ) ))& index(status,host(X)) = elec_1 )=> ( leq(nbr_proc,host(X))=> (! [Z] :( ~ setIn(host(Z),setEmpty)=> (! [V0] :( host(X) = host(V0)=> (! [W0] :( host(X) != host(W0)=> ( ( setIn(V0,alive)& setIn(W0,alive)& host(X) = host(V0)& index(ldr,host(W0)) = host(W0)& index(status,host(W0)) = norm )=> W0 = V0 ) ) )) )) )) ) ) ) ) ) )),
% 203.34/26.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 203.34/26.57 fof(f68,negated_conjecture,(
% 203.34/26.57 ~((! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),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,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm& index(status,host(Pid0)) = norm& index(ldr,host(Pid0)) = host(Pid0) )=> Pid0 = Z ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& leq(nbr_proc,index(pendack,host(Pid0)))& index(status,host(Pid0)) = elec_2& host(Pid20) = index(pendack,host(Pid0)) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))& leq(nbr_proc,index(pendack,host(Pid0)))& index(status,host(Pid0)) = elec_2& host(Pid20) = index(pendack,host(Pid0)) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& ~ leq(host(Pid0),host(Z))& elem(m_Down(Pid20),queue(host(Pid0)))& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Down(Y),V) )=> ( setIn(X,alive)=> ( ~ leq(host(X),host(Y))=> ( ~ ( ( index(ldr,host(X)) = host(Y)& index(status,host(X)) = norm )| ( index(status,host(X)) = wait& host(Y) = host(index(elid,host(X))) ) )=> ( ( (! [Z] :( ( ~ leq(host(X),Z)& leq(s(zero),Z) )=> ( setIn(Z,index(down,host(X)))| Z = host(Y) ) ))& index(status,host(X)) = elec_1 )=> ( leq(nbr_proc,host(X))=> (! [Z] :( ~ setIn(host(Z),setEmpty)=> (! [V0] :( host(X) = host(V0)=> (! [W0] :( host(X) != host(W0)=> ( ( setIn(V0,alive)& setIn(W0,alive)& host(X) = host(V0)& index(ldr,host(W0)) = host(W0)& index(status,host(W0)) = norm )=> W0 = V0 ) ) )) )) )) ) ) ) ) ) ))),
% 203.34/26.57 inference(negated_conjecture,[status(cth)],[f67])).
% 203.34/26.57 fof(f72,plain,(
% 203.34/26.57 ![P,Q]: (~s(host(P))=host(Q)|~host(P)=host(Q))),
% 203.34/26.57 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 203.34/26.57 fof(f73,plain,(
% 203.34/26.57 ![X0,X1]: (~s(host(X0))=host(X1)|~host(X0)=host(X1))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f72])).
% 203.34/26.57 fof(f74,plain,(
% 203.34/26.57 ![X0]: (leq(s(zero),host(X0)))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f3])).
% 203.34/26.57 fof(f75,plain,(
% 203.34/26.57 leq(s(zero),nbr_proc)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f4])).
% 203.34/26.57 fof(f76,plain,(
% 203.34/26.57 ![X0]: (leq(host(X0),nbr_proc))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f5])).
% 203.34/26.57 fof(f83,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_Halt(X2))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f12])).
% 203.34/26.57 fof(f84,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_Down(X2))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f13])).
% 203.34/26.57 fof(f128,plain,(
% 203.34/26.57 ![X0,X1]: (tail(cons(X0,X1))=X1)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f37])).
% 203.34/26.57 fof(f133,plain,(
% 203.34/26.57 ![X0,X1]: (~q_nil=cons(X0,X1))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f42])).
% 203.34/26.57 fof(f134,plain,(
% 203.34/26.57 ![X0,X1]: (~q_nil=snoc(X0,X1))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f43])).
% 203.34/26.57 fof(f138,plain,(
% 203.34/26.57 ![X,Y,Q]: ((~elem(X,cons(Y,Q))|(X=Y|elem(X,Q)))&(elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 203.34/26.57 inference(NNF_transformation,[status(thm)],[f47])).
% 203.34/26.57 fof(f139,plain,(
% 203.34/26.57 (![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))))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f138])).
% 203.34/26.57 fof(f141,plain,(
% 203.34/26.57 ![X0,X1,X2]: (elem(X0,cons(X1,X2))|~X0=X1)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f139])).
% 203.34/26.57 fof(f148,plain,(
% 203.34/26.57 ![X]: ((~pidElem(X)|(?[Y]: (X=m_Halt(Y)|X=m_Down(Y))))&(pidElem(X)|(![Y]: (~X=m_Halt(Y)&~X=m_Down(Y)))))),
% 203.34/26.57 inference(NNF_transformation,[status(thm)],[f49])).
% 203.34/26.57 fof(f149,plain,(
% 203.34/26.57 (![X]: (~pidElem(X)|((?[Y]: X=m_Halt(Y))|(?[Y]: X=m_Down(Y)))))&(![X]: (pidElem(X)|((![Y]: ~X=m_Halt(Y))&(![Y]: ~X=m_Down(Y)))))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f148])).
% 203.34/26.57 fof(f150,plain,(
% 203.34/26.57 (![X]: (~pidElem(X)|(X=m_Halt(sK0_skl(X))|X=m_Down(sK1_skl(X)))))&(![X]: (pidElem(X)|((![Y]: ~X=m_Halt(Y))&(![Y]: ~X=m_Down(Y)))))),
% 203.34/26.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl(X)),skolemize(Y,sK1_skl(X))],[f149])).
% 203.34/26.57 fof(f151,plain,(
% 203.34/26.57 ![X0]: (~pidElem(X0)|X0=m_Halt(sK0_skl(X0))|X0=m_Down(sK1_skl(X0)))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f150])).
% 203.34/26.57 fof(f155,plain,(
% 203.34/26.57 ![X0]: (pidMsg(m_Down(X0))=X0)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f51])).
% 203.34/26.57 fof(f157,plain,(
% 203.34/26.57 (![X]: ordered(cons(X,q_nil)))&(![X]: ordered(snoc(q_nil,X)))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f53])).
% 203.34/26.57 fof(f158,plain,(
% 203.34/26.57 ![X0]: (ordered(cons(X0,q_nil)))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f157])).
% 203.34/26.57 fof(f191,plain,(
% 203.34/26.57 ![X0]: (~leq(s(X0),X0))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f59])).
% 203.34/26.57 fof(f192,plain,(
% 203.34/26.57 ![X0]: (leq(X0,X0))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f60])).
% 203.34/26.57 fof(f193,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,X1)|leq(X1,X0))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f61])).
% 203.34/26.57 fof(f194,plain,(
% 203.34/26.57 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 203.34/26.57 inference(NNF_transformation,[status(thm)],[f62])).
% 203.34/26.57 fof(f195,plain,(
% 203.34/26.57 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f194])).
% 203.34/26.57 fof(f196,plain,(
% 203.34/26.57 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f195])).
% 203.34/26.57 fof(f199,plain,(
% 203.34/26.57 ![X,Y,Z]: ((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))),
% 203.34/26.57 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 203.34/26.57 fof(f200,plain,(
% 203.34/26.57 ![X,Z]: ((![Y]: (~leq(X,Y)|~leq(Y,Z)))|leq(X,Z))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f199])).
% 203.34/26.57 fof(f201,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f200])).
% 203.34/26.57 fof(f202,plain,(
% 203.34/26.57 ![X,Y]: ((~leq(X,Y)|leq(s(X),s(Y)))&(leq(X,Y)|~leq(s(X),s(Y))))),
% 203.34/26.57 inference(NNF_transformation,[status(thm)],[f64])).
% 203.34/26.57 fof(f203,plain,(
% 203.34/26.57 (![X,Y]: (~leq(X,Y)|leq(s(X),s(Y))))&(![X,Y]: (leq(X,Y)|~leq(s(X),s(Y))))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f202])).
% 203.34/26.57 fof(f204,plain,(
% 203.34/26.57 ![X0,X1]: (~leq(X0,X1)|leq(s(X0),s(X1)))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f203])).
% 203.34/26.57 fof(f205,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,X1)|~leq(s(X0),s(X1)))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f203])).
% 203.34/26.57 fof(f206,plain,(
% 203.34/26.57 ![X,Y]: ((~leq(X,s(Y))|(X=s(Y)|leq(X,Y)))&(leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 203.34/26.57 inference(NNF_transformation,[status(thm)],[f65])).
% 203.34/26.57 fof(f207,plain,(
% 203.34/26.57 (![X,Y]: (~leq(X,s(Y))|(X=s(Y)|leq(X,Y))))&(![X,Y]: (leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f206])).
% 203.34/26.57 fof(f210,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,s(X1))|~leq(X0,X1))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f207])).
% 203.34/26.57 fof(f212,plain,(
% 203.34/26.57 (?[V,W,X,Y]: (((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),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,Pid0]: ((((((~setIn(Z,alive)|~setIn(Pid0,alive))|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|Pid0=Z)))&(![Z,Pid20,Pid0]: (((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Pid20)=index(pendack,host(Pid0)))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid20,Pid0]: (((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Pid20),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Pid20)=index(pendack,host(Pid0)))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid20,Pid0]: (((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|leq(host(Pid0),host(Z)))|~elem(m_Down(Pid20),queue(host(Pid0))))|~index(status,host(Pid0))=elec_1)|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(X))=cons(m_Down(Y),V))&(setIn(X,alive)&(~leq(host(X),host(Y))&(((~index(ldr,host(X))=host(Y)|~index(status,host(X))=norm)&(~index(status,host(X))=wait|~host(Y)=host(index(elid,host(X)))))&(((![Z]: ((leq(host(X),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(X)))|Z=host(Y))))&index(status,host(X))=elec_1)&(leq(nbr_proc,host(X))&(?[Z]: (~setIn(host(Z),setEmpty)&(?[V0]: (host(X)=host(V0)&(?[W0]: (~host(X)=host(W0)&(((((setIn(V0,alive)&setIn(W0,alive))&host(X)=host(V0))&index(ldr,host(W0))=host(W0))&index(status,host(W0))=norm)&~W0=V0))))))))))))))),
% 203.34/26.57 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 203.34/26.57 fof(f213,plain,(
% 203.34/26.57 ?[X,Y]: (((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),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,Pid0]: ((((((~setIn(Z,alive)|~setIn(Pid0,alive))|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|Pid0=Z)))&((![Pid20,Pid0]: ((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Pid20)=index(pendack,host(Pid0))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&((![Pid20,Pid0]: ((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Pid20),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Pid20)=index(pendack,host(Pid0))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z]: ((![Pid0]: ((![Pid20]: (((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|leq(host(Pid0),host(Z)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~index(status,host(Pid0))=elec_1))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(?[V]: queue(host(X))=cons(m_Down(Y),V)))&(setIn(X,alive)&(~leq(host(X),host(Y))&(((~index(ldr,host(X))=host(Y)|~index(status,host(X))=norm)&(~index(status,host(X))=wait|~host(Y)=host(index(elid,host(X)))))&(((![Z]: ((leq(host(X),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(X)))|Z=host(Y))))&index(status,host(X))=elec_1)&(leq(nbr_proc,host(X))&((?[Z]: ~setIn(host(Z),setEmpty))&(?[V0]: (host(X)=host(V0)&(?[W0]: (~host(X)=host(W0)&(((((setIn(V0,alive)&setIn(W0,alive))&host(X)=host(V0))&index(ldr,host(W0))=host(W0))&index(status,host(W0))=norm)&~W0=V0))))))))))))),
% 203.34/26.57 inference(miniscoping,[status(thm)],[f212])).
% 203.34/26.57 fof(f214,plain,(
% 203.34/26.57 (((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),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,Pid0]: ((((((~setIn(Z,alive)|~setIn(Pid0,alive))|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm)|~index(status,host(Pid0))=norm)|~index(ldr,host(Pid0))=host(Pid0))|Pid0=Z)))&((![Pid20,Pid0]: ((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Pid20)=index(pendack,host(Pid0))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&((![Pid20,Pid0]: ((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Pid20),queue(host(Pid0))))|~leq(nbr_proc,index(pendack,host(Pid0))))|~index(status,host(Pid0))=elec_2)|~host(Pid20)=index(pendack,host(Pid0))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z]: ((![Pid0]: ((![Pid20]: ((((~leq(host(Pid0),sK6_skl(Pid20,Pid0,Z))&leq(s(zero),sK6_skl(Pid20,Pid0,Z)))&(~setIn(sK6_skl(Pid20,Pid0,Z),index(down,host(Pid0)))&~sK6_skl(Pid20,Pid0,Z)=host(Pid20)))|leq(host(Pid0),host(Z)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~index(status,host(Pid0))=elec_1))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(sK4_skl))=cons(m_Down(sK5_skl),sK7_skl))&(setIn(sK4_skl,alive)&(~leq(host(sK4_skl),host(sK5_skl))&(((~index(ldr,host(sK4_skl))=host(sK5_skl)|~index(status,host(sK4_skl))=norm)&(~index(status,host(sK4_skl))=wait|~host(sK5_skl)=host(index(elid,host(sK4_skl)))))&(((![Z]: ((leq(host(sK4_skl),Z)|~leq(s(zero),Z))|(setIn(Z,index(down,host(sK4_skl)))|Z=host(sK5_skl))))&index(status,host(sK4_skl))=elec_1)&(leq(nbr_proc,host(sK4_skl))&(~setIn(host(sK8_skl),setEmpty)&(host(sK4_skl)=host(sK9_skl)&(~host(sK4_skl)=host(sK10_skl)&(((((setIn(sK9_skl,alive)&setIn(sK10_skl,alive))&host(sK4_skl)=host(sK9_skl))&index(ldr,host(sK10_skl))=host(sK10_skl))&index(status,host(sK10_skl))=norm)&~sK10_skl=sK9_skl))))))))))),
% 203.34/26.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(V0,sK6_skl(Pid20,Pid0,Z)),skolemize(V,sK7_skl),skolemize(Z,sK8_skl),skolemize(V0,sK9_skl),skolemize(W0,sK10_skl)],[f213])).
% 203.34/26.57 fof(f222,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~leq(host(X0),sK6_skl(X1,X0,X2))|leq(host(X0),host(X2))|~elem(m_Down(X1),queue(host(X0)))|~index(status,host(X0))=elec_1|~setIn(X2,alive)|~index(ldr,host(X2))=host(X2)|~index(status,host(X2))=norm)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f223,plain,(
% 203.34/26.57 ![X0,X1,X2]: (leq(s(zero),sK6_skl(X0,X1,X2))|leq(host(X1),host(X2))|~elem(m_Down(X0),queue(host(X1)))|~index(status,host(X1))=elec_1|~setIn(X2,alive)|~index(ldr,host(X2))=host(X2)|~index(status,host(X2))=norm)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f224,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~setIn(sK6_skl(X0,X1,X2),index(down,host(X1)))|leq(host(X1),host(X2))|~elem(m_Down(X0),queue(host(X1)))|~index(status,host(X1))=elec_1|~setIn(X2,alive)|~index(ldr,host(X2))=host(X2)|~index(status,host(X2))=norm)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f225,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~sK6_skl(X0,X1,X2)=host(X0)|leq(host(X1),host(X2))|~elem(m_Down(X0),queue(host(X1)))|~index(status,host(X1))=elec_1|~setIn(X2,alive)|~index(ldr,host(X2))=host(X2)|~index(status,host(X2))=norm)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f226,plain,(
% 203.34/26.57 queue(host(sK4_skl))=cons(m_Down(sK5_skl),sK7_skl)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f227,plain,(
% 203.34/26.57 setIn(sK4_skl,alive)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f231,plain,(
% 203.34/26.57 ![X0]: (leq(host(sK4_skl),X0)|~leq(s(zero),X0)|setIn(X0,index(down,host(sK4_skl)))|X0=host(sK5_skl))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f232,plain,(
% 203.34/26.57 index(status,host(sK4_skl))=elec_1),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f233,plain,(
% 203.34/26.57 leq(nbr_proc,host(sK4_skl))),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f236,plain,(
% 203.34/26.57 ~host(sK4_skl)=host(sK10_skl)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f238,plain,(
% 203.34/26.57 setIn(sK10_skl,alive)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f240,plain,(
% 203.34/26.57 index(ldr,host(sK10_skl))=host(sK10_skl)),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f241,plain,(
% 203.34/26.57 index(status,host(sK10_skl))=norm),
% 203.34/26.57 inference(cnf_transformation,[status(thm)],[f214])).
% 203.34/26.57 fof(f268,plain,(
% 203.34/26.57 ![X0,X1]: (elem(X0,cons(X0,X1)))),
% 203.34/26.57 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 203.34/26.57 fof(f295,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(X0)),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f210,f191])).
% 203.34/26.57 fof(f313,definition,(
% 203.34/26.57 sQ13_spl <=> (index(status,host(sK4_skl))=elec_1)),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f315,plain,(
% 203.34/26.57 ~index(status,host(sK4_skl))=elec_1|sQ13_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f313])).
% 203.34/26.57 fof(f320,plain,(
% 203.34/26.57 ~elec_1=elec_1|sQ13_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f232,f315])).
% 203.34/26.57 fof(f321,plain,(
% 203.34/26.57 $false|sQ13_spl),
% 203.34/26.57 inference(trivial_equality_resolution,[status(thm)],[f320])).
% 203.34/26.57 fof(f322,plain,(
% 203.34/26.57 sQ13_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f321])).
% 203.34/26.57 fof(f329,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(X0))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f295,f210])).
% 203.34/26.57 fof(f335,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(s(X0)))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f329,f210])).
% 203.34/26.57 fof(f340,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,X1)|~leq(s(X0),X1))),
% 203.34/26.57 inference(resolution,[status(thm)],[f205,f210])).
% 203.34/26.57 fof(f356,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,s(X1))|~leq(s(X0),X1))),
% 203.34/26.57 inference(resolution,[status(thm)],[f340,f210])).
% 203.34/26.57 fof(f357,plain,(
% 203.34/26.57 ![X0]: (leq(X0,s(X0)))),
% 203.34/26.57 inference(resolution,[status(thm)],[f340,f192])).
% 203.34/26.57 fof(f359,plain,(
% 203.34/26.57 ![X0]: (leq(X0,s(s(X0))))),
% 203.34/26.57 inference(resolution,[status(thm)],[f357,f340])).
% 203.34/26.57 fof(f365,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(s(s(X0))))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f335,f210])).
% 203.34/26.57 fof(f368,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,s(s(X1)))|~leq(X0,X1))),
% 203.34/26.57 inference(resolution,[status(thm)],[f356,f204])).
% 203.34/26.57 fof(f388,definition,(
% 203.34/26.57 sQ20_spl <=> (index(status,host(sK10_skl))=norm)),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f390,plain,(
% 203.34/26.57 ~index(status,host(sK10_skl))=norm|sQ20_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f388])).
% 203.34/26.57 fof(f391,definition,(
% 203.34/26.57 sQ21_spl <=> (index(ldr,host(sK10_skl))=host(sK10_skl))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f393,plain,(
% 203.34/26.57 ~index(ldr,host(sK10_skl))=host(sK10_skl)|sQ21_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f391])).
% 203.34/26.57 fof(f403,plain,(
% 203.34/26.57 ~host(sK10_skl)=host(sK10_skl)|sQ21_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f240,f393])).
% 203.34/26.57 fof(f404,plain,(
% 203.34/26.57 $false|sQ21_spl),
% 203.34/26.57 inference(trivial_equality_resolution,[status(thm)],[f403])).
% 203.34/26.57 fof(f405,plain,(
% 203.34/26.57 sQ21_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f404])).
% 203.34/26.57 fof(f406,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(s(s(s(X0)))))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f368,f335])).
% 203.34/26.57 fof(f455,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(s(s(s(s(X0))))))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f365,f368])).
% 203.34/26.57 fof(f503,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(s(s(s(s(s(X0)))))))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f406,f368])).
% 203.34/26.57 fof(f515,plain,(
% 203.34/26.57 elem(m_Down(sK5_skl),queue(host(sK4_skl)))),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f226,f268])).
% 203.34/26.57 fof(f557,plain,(
% 203.34/26.57 ![X0]: (~leq(host(sK4_skl),sK6_skl(sK5_skl,sK4_skl,X0))|leq(host(sK4_skl),host(X0))|~index(status,host(sK4_skl))=elec_1|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm)),
% 203.34/26.57 inference(resolution,[status(thm)],[f515,f222])).
% 203.34/26.57 fof(f558,definition,(
% 203.34/26.57 ![X0]: (sQ30_spl <=> (~leq(host(sK4_skl),sK6_skl(sK5_skl,sK4_skl,X0))|leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f559,plain,(
% 203.34/26.57 ![X0]: (~leq(host(sK4_skl),sK6_skl(sK5_skl,sK4_skl,X0))|leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ30_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f558])).
% 203.34/26.57 fof(f561,plain,(
% 203.34/26.57 sQ30_spl|~sQ13_spl),
% 203.34/26.57 inference(split_clause,[status(thm)],[f557,f558,f313])).
% 203.34/26.57 fof(f578,plain,(
% 203.34/26.57 ![X0]: (leq(s(zero),sK6_skl(sK5_skl,sK4_skl,X0))|leq(host(sK4_skl),host(X0))|~index(status,host(sK4_skl))=elec_1|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm)),
% 203.34/26.57 inference(resolution,[status(thm)],[f223,f515])).
% 203.34/26.57 fof(f579,definition,(
% 203.34/26.57 ![X0]: (sQ31_spl <=> (leq(s(zero),sK6_skl(sK5_skl,sK4_skl,X0))|leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f580,plain,(
% 203.34/26.57 ![X0]: (leq(s(zero),sK6_skl(sK5_skl,sK4_skl,X0))|leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ31_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f579])).
% 203.34/26.57 fof(f582,plain,(
% 203.34/26.57 sQ31_spl|~sQ13_spl),
% 203.34/26.57 inference(split_clause,[status(thm)],[f578,f579,f313])).
% 203.34/26.57 fof(f585,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(s(s(s(s(s(s(X0))))))))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f455,f368])).
% 203.34/26.57 fof(f598,definition,(
% 203.34/26.57 sQ32_spl <=> (s(zero)=s(s(s(s(nbr_proc)))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f599,plain,(
% 203.34/26.57 s(zero)=s(s(s(s(nbr_proc))))|~sQ32_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f598])).
% 203.34/26.57 fof(f614,plain,(
% 203.34/26.57 ![X0]: (~leq(s(s(s(s(s(s(s(s(s(s(X0)))))))))),X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f503,f368])).
% 203.34/26.57 fof(f760,plain,(
% 203.34/26.57 ![X0,X1]: (leq(s(X0),s(X1))|leq(X1,X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f193,f205])).
% 203.34/26.57 fof(f766,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,s(X1))|leq(X1,s(X0)))),
% 203.34/26.57 inference(resolution,[status(thm)],[f193,f356])).
% 203.34/26.57 fof(f834,plain,(
% 203.34/26.57 ![X0]: (~sK6_skl(sK5_skl,sK4_skl,X0)=host(sK5_skl)|leq(host(sK4_skl),host(X0))|~index(status,host(sK4_skl))=elec_1|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm)),
% 203.34/26.57 inference(resolution,[status(thm)],[f225,f515])).
% 203.34/26.57 fof(f835,definition,(
% 203.34/26.57 ![X0]: (sQ39_spl <=> (~sK6_skl(sK5_skl,sK4_skl,X0)=host(sK5_skl)|leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f836,plain,(
% 203.34/26.57 ![X0]: (~sK6_skl(sK5_skl,sK4_skl,X0)=host(sK5_skl)|leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ39_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f835])).
% 203.34/26.57 fof(f838,plain,(
% 203.34/26.57 sQ39_spl|~sQ13_spl),
% 203.34/26.57 inference(split_clause,[status(thm)],[f834,f835,f313])).
% 203.34/26.57 fof(f941,plain,(
% 203.34/26.57 ![X0]: (~leq(nbr_proc,host(X0))|nbr_proc=host(X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f196,f76])).
% 203.34/26.57 fof(f942,plain,(
% 203.34/26.57 ~leq(host(sK4_skl),nbr_proc)|host(sK4_skl)=nbr_proc),
% 203.34/26.57 inference(resolution,[status(thm)],[f196,f233])).
% 203.34/26.57 fof(f986,definition,(
% 203.34/26.57 sQ50_spl <=> (leq(host(sK4_skl),nbr_proc))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f988,plain,(
% 203.34/26.57 ~leq(host(sK4_skl),nbr_proc)|sQ50_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f986])).
% 203.34/26.57 fof(f989,definition,(
% 203.34/26.57 sQ51_spl <=> (host(sK4_skl)=nbr_proc)),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f990,plain,(
% 203.34/26.57 host(sK4_skl)=nbr_proc|~sQ51_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f989])).
% 203.34/26.57 fof(f992,plain,(
% 203.34/26.57 ~sQ50_spl|sQ51_spl),
% 203.34/26.57 inference(split_clause,[status(thm)],[f942,f986,f989])).
% 203.34/26.57 fof(f1004,plain,(
% 203.34/26.57 $false|sQ50_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f988,f76])).
% 203.34/26.57 fof(f1005,plain,(
% 203.34/26.57 sQ50_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f1004])).
% 203.34/26.57 fof(f1014,plain,(
% 203.34/26.57 ![X0,X1]: (~leq(s(s(X0)),X1)|~leq(X1,X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f201,f295])).
% 203.34/26.57 fof(f1015,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~leq(s(X0),X1)|~leq(X1,s(X2))|leq(X0,X2))),
% 203.34/26.57 inference(resolution,[status(thm)],[f201,f205])).
% 203.34/26.57 fof(f1018,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~leq(s(X0),X1)|~leq(X1,X2)|leq(X0,s(X2)))),
% 203.34/26.57 inference(resolution,[status(thm)],[f201,f356])).
% 203.34/26.57 fof(f1020,plain,(
% 203.34/26.57 ![X0,X1]: (~leq(s(X0),X1)|~leq(X1,X0))),
% 203.34/26.57 inference(resolution,[status(thm)],[f201,f191])).
% 203.34/26.57 fof(f1032,plain,(
% 203.34/26.57 ![X0]: (~leq(host(X0),zero))),
% 203.34/26.57 inference(resolution,[status(thm)],[f1020,f74])).
% 203.34/26.57 fof(f1141,plain,(
% 203.34/26.57 ![X0,X1]: (leq(host(sK4_skl),sK6_skl(X0,sK4_skl,X1))|~leq(s(zero),sK6_skl(X0,sK4_skl,X1))|sK6_skl(X0,sK4_skl,X1)=host(sK5_skl)|leq(host(sK4_skl),host(X1))|~elem(m_Down(X0),queue(host(sK4_skl)))|~index(status,host(sK4_skl))=elec_1|~setIn(X1,alive)|~index(ldr,host(X1))=host(X1)|~index(status,host(X1))=norm)),
% 203.34/26.57 inference(resolution,[status(thm)],[f231,f224])).
% 203.34/26.57 fof(f1142,definition,(
% 203.34/26.57 ![X0,X1]: (sQ57_spl <=> (leq(host(sK4_skl),sK6_skl(X0,sK4_skl,X1))|~leq(s(zero),sK6_skl(X0,sK4_skl,X1))|sK6_skl(X0,sK4_skl,X1)=host(sK5_skl)|leq(host(sK4_skl),host(X1))|~elem(m_Down(X0),queue(host(sK4_skl)))|~setIn(X1,alive)|~index(ldr,host(X1))=host(X1)|~index(status,host(X1))=norm))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f1143,plain,(
% 203.34/26.57 ![X0,X1]: (leq(host(sK4_skl),sK6_skl(X0,sK4_skl,X1))|~leq(s(zero),sK6_skl(X0,sK4_skl,X1))|sK6_skl(X0,sK4_skl,X1)=host(sK5_skl)|leq(host(sK4_skl),host(X1))|~elem(m_Down(X0),queue(host(sK4_skl)))|~setIn(X1,alive)|~index(ldr,host(X1))=host(X1)|~index(status,host(X1))=norm|~sQ57_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f1142])).
% 203.34/26.57 fof(f1145,plain,(
% 203.34/26.57 sQ57_spl|~sQ13_spl),
% 203.34/26.57 inference(split_clause,[status(thm)],[f1141,f1142,f313])).
% 203.34/26.57 fof(f1217,plain,(
% 203.34/26.57 ~norm=norm|sQ20_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f241,f390])).
% 203.34/26.57 fof(f1218,plain,(
% 203.34/26.57 $false|sQ20_spl),
% 203.34/26.57 inference(trivial_equality_resolution,[status(thm)],[f1217])).
% 203.34/26.57 fof(f1219,plain,(
% 203.34/26.57 sQ20_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f1218])).
% 203.34/26.57 fof(f1423,definition,(
% 203.34/26.57 sQ60_spl <=> (setIn(sK4_skl,alive))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f1425,plain,(
% 203.34/26.57 ~setIn(sK4_skl,alive)|sQ60_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f1423])).
% 203.34/26.57 fof(f2239,definition,(
% 203.34/26.57 sQ87_spl <=> (host(sK4_skl)=host(sK4_skl))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f2241,plain,(
% 203.34/26.57 ~host(sK4_skl)=host(sK4_skl)|sQ87_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f2239])).
% 203.34/26.57 fof(f2378,definition,(
% 203.34/26.57 sQ96_spl <=> (host(sK5_skl)=s(nbr_proc))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f2379,plain,(
% 203.34/26.57 host(sK5_skl)=s(nbr_proc)|~sQ96_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f2378])).
% 203.34/26.57 fof(f2435,plain,(
% 203.34/26.57 ~leq(host(sK5_skl),nbr_proc)|~sQ96_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f2379,f191])).
% 203.34/26.57 fof(f2442,plain,(
% 203.34/26.57 $false|~sQ96_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f2435,f76])).
% 203.34/26.57 fof(f2443,plain,(
% 203.34/26.57 ~sQ96_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f2442])).
% 203.34/26.57 fof(f2668,definition,(
% 203.34/26.57 ![X0]: (sQ98_spl <=> (~ordered(cons(X0,q_nil))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f2669,plain,(
% 203.34/26.57 ![X0]: (~ordered(cons(X0,q_nil))|~sQ98_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f2668])).
% 203.34/26.57 fof(f2675,plain,(
% 203.34/26.57 $false|~sQ98_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f2669,f158])).
% 203.34/26.57 fof(f2676,plain,(
% 203.34/26.57 ~sQ98_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f2675])).
% 203.34/26.57 fof(f2829,plain,(
% 203.34/26.57 ~leq(s(zero),nbr_proc)|~sQ32_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f599,f335])).
% 203.34/26.57 fof(f2915,definition,(
% 203.34/26.57 sQ106_spl <=> (zero=s(s(s(s(nbr_proc)))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f2916,plain,(
% 203.34/26.57 zero=s(s(s(s(nbr_proc))))|~sQ106_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f2915])).
% 203.34/26.57 fof(f2929,plain,(
% 203.34/26.57 ~leq(s(zero),nbr_proc)|~sQ106_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f2916,f365])).
% 203.34/26.57 fof(f3073,plain,(
% 203.34/26.57 $false|~sQ32_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f2829,f75])).
% 203.34/26.57 fof(f3074,plain,(
% 203.34/26.57 ~sQ32_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f3073])).
% 203.34/26.57 fof(f3183,plain,(
% 203.34/26.57 elem(m_Down(sK5_skl),queue(nbr_proc))|~sQ51_spl),
% 203.34/26.57 inference(backward_demodulation,[status(thm)],[f990,f515])).
% 203.34/26.57 fof(f3184,plain,(
% 203.34/26.57 ~nbr_proc=host(sK10_skl)|~sQ51_spl),
% 203.34/26.57 inference(backward_demodulation,[status(thm)],[f990,f236])).
% 203.34/26.57 fof(f3369,definition,(
% 203.34/26.57 sQ125_spl <=> (q_nil=cons(m_Down(sK5_skl),tail(q_nil)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f3370,plain,(
% 203.34/26.57 q_nil=cons(m_Down(sK5_skl),tail(q_nil))|~sQ125_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f3369])).
% 203.34/26.57 fof(f3375,plain,(
% 203.34/26.57 $false|sQ60_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f1425,f227])).
% 203.34/26.57 fof(f3376,plain,(
% 203.34/26.57 sQ60_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f3375])).
% 203.34/26.57 fof(f3386,plain,(
% 203.34/26.57 $false|~sQ125_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f3370,f133])).
% 203.34/26.57 fof(f3387,plain,(
% 203.34/26.57 ~sQ125_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f3386])).
% 203.34/26.57 fof(f3461,plain,(
% 203.34/26.57 ![X0,X1]: (leq(nbr_proc,sK6_skl(X0,sK4_skl,X1))|~leq(s(zero),sK6_skl(X0,sK4_skl,X1))|sK6_skl(X0,sK4_skl,X1)=host(sK5_skl)|leq(host(sK4_skl),host(X1))|~elem(m_Down(X0),queue(host(sK4_skl)))|~setIn(X1,alive)|~index(ldr,host(X1))=host(X1)|~index(status,host(X1))=norm|~sQ51_spl|~sQ57_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f990,f1143])).
% 203.34/26.57 fof(f3462,plain,(
% 203.34/26.57 ![X0,X1]: (leq(nbr_proc,sK6_skl(X0,sK4_skl,X1))|~leq(s(zero),sK6_skl(X0,sK4_skl,X1))|sK6_skl(X0,sK4_skl,X1)=host(sK5_skl)|leq(nbr_proc,host(X1))|~elem(m_Down(X0),queue(host(sK4_skl)))|~setIn(X1,alive)|~index(ldr,host(X1))=host(X1)|~index(status,host(X1))=norm|~sQ51_spl|~sQ57_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f990,f3461])).
% 203.34/26.57 fof(f3463,plain,(
% 203.34/26.57 ![X0,X1]: (leq(nbr_proc,sK6_skl(X0,sK4_skl,X1))|~leq(s(zero),sK6_skl(X0,sK4_skl,X1))|sK6_skl(X0,sK4_skl,X1)=host(sK5_skl)|leq(nbr_proc,host(X1))|~elem(m_Down(X0),queue(nbr_proc))|~setIn(X1,alive)|~index(ldr,host(X1))=host(X1)|~index(status,host(X1))=norm|~sQ51_spl|~sQ57_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f990,f3462])).
% 203.34/26.57 fof(f3464,plain,(
% 203.34/26.57 ![X0]: (leq(nbr_proc,sK6_skl(sK5_skl,sK4_skl,X0))|~leq(s(zero),sK6_skl(sK5_skl,sK4_skl,X0))|sK6_skl(sK5_skl,sK4_skl,X0)=host(sK5_skl)|leq(nbr_proc,host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ57_spl|~sQ51_spl)),
% 203.34/26.57 inference(resolution,[status(thm)],[f3463,f3183])).
% 203.34/26.57 fof(f3513,plain,(
% 203.34/26.57 ![X0,X1,X2]: (~leq(s(X0),s(X1))|leq(X2,X1)|leq(X0,X2))),
% 203.34/26.57 inference(resolution,[status(thm)],[f1015,f760])).
% 203.34/26.57 fof(f3521,plain,(
% 203.34/26.57 ![X0,X1]: (~leq(s(s(X0)),s(X1))|leq(X0,X1))),
% 203.34/26.57 inference(resolution,[status(thm)],[f1015,f766])).
% 203.34/26.57 fof(f3709,plain,(
% 203.34/26.57 $false|~sQ106_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f2929,f75])).
% 203.34/26.57 fof(f3710,plain,(
% 203.34/26.57 ~sQ106_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f3709])).
% 203.34/26.57 fof(f4207,definition,(
% 203.34/26.57 sQ165_spl <=> (host(sK5_skl)=s(s(s(nbr_proc))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f4208,plain,(
% 203.34/26.57 host(sK5_skl)=s(s(s(nbr_proc)))|~sQ165_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f4207])).
% 203.34/26.57 fof(f4247,plain,(
% 203.34/26.57 ~leq(host(sK5_skl),nbr_proc)|~sQ165_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f4208,f329])).
% 203.34/26.57 fof(f4398,definition,(
% 203.34/26.57 sQ169_spl <=> (leq(s(zero),s(zero)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f4400,plain,(
% 203.34/26.57 ~leq(s(zero),s(zero))|sQ169_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f4398])).
% 203.34/26.57 fof(f4468,definition,(
% 203.34/26.57 sQ173_spl <=> (leq(host(sK5_skl),host(sK5_skl)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f4470,plain,(
% 203.34/26.57 ~leq(host(sK5_skl),host(sK5_skl))|sQ173_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f4468])).
% 203.34/26.57 fof(f4655,definition,(
% 203.34/26.57 sQ177_spl <=> (leq(nbr_proc,s(nbr_proc)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f4657,plain,(
% 203.34/26.57 ~leq(nbr_proc,s(nbr_proc))|sQ177_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f4655])).
% 203.34/26.57 fof(f5037,definition,(
% 203.34/26.57 ![X0]: (sQ187_spl <=> (pidElem(X0)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f5038,plain,(
% 203.34/26.57 ![X0]: (pidElem(X0)|~sQ187_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f5037])).
% 203.34/26.57 fof(f5220,plain,(
% 203.34/26.57 ![X0,X1]: (leq(X0,X1)|leq(s(X1),s(s(X0))))),
% 203.34/26.57 inference(resolution,[status(thm)],[f3521,f193])).
% 203.34/26.57 fof(f5393,definition,(
% 203.34/26.57 sQ191_spl <=> (leq(zero,zero))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f5395,plain,(
% 203.34/26.57 ~leq(zero,zero)|sQ191_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f5393])).
% 203.34/26.57 fof(f5492,definition,(
% 203.34/26.57 sQ192_spl <=> (leq(s(nbr_proc),s(nbr_proc)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f5494,plain,(
% 203.34/26.57 ~leq(s(nbr_proc),s(nbr_proc))|sQ192_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f5492])).
% 203.34/26.57 fof(f6113,plain,(
% 203.34/26.57 ![X0]: (~leq(nbr_proc,sK6_skl(sK5_skl,sK4_skl,X0))|leq(host(sK4_skl),host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ51_spl|~sQ30_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f990,f559])).
% 203.34/26.57 fof(f6114,plain,(
% 203.34/26.57 ![X0]: (~leq(nbr_proc,sK6_skl(sK5_skl,sK4_skl,X0))|leq(nbr_proc,host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ51_spl|~sQ30_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f990,f6113])).
% 203.34/26.57 fof(f6120,definition,(
% 203.34/26.57 sQ197_spl <=> (leq(nbr_proc,host(sK10_skl)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6121,plain,(
% 203.34/26.57 leq(nbr_proc,host(sK10_skl))|~sQ197_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f6120])).
% 203.34/26.57 fof(f6151,definition,(
% 203.34/26.57 sQ203_spl <=> (host(sK5_skl)=s(s(s(s(nbr_proc)))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6152,plain,(
% 203.34/26.57 host(sK5_skl)=s(s(s(s(nbr_proc))))|~sQ203_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f6151])).
% 203.34/26.57 fof(f6172,plain,(
% 203.34/26.57 ~leq(host(sK5_skl),nbr_proc)|~sQ203_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f6152,f335])).
% 203.34/26.57 fof(f6290,plain,(
% 203.34/26.57 nbr_proc=host(sK10_skl)|~sQ197_spl),
% 203.34/26.57 inference(resolution,[status(thm)],[f6121,f941])).
% 203.34/26.57 fof(f6295,plain,(
% 203.34/26.57 $false|~sQ51_spl|~sQ197_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f6290,f3184])).
% 203.34/26.57 fof(f6296,plain,(
% 203.34/26.57 ~sQ51_spl|~sQ197_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f6295])).
% 203.34/26.57 fof(f6323,plain,(
% 203.34/26.57 ![X0]: (~sK6_skl(sK5_skl,sK4_skl,X0)=host(sK5_skl)|leq(nbr_proc,host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ51_spl|~sQ39_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f990,f836])).
% 203.34/26.57 fof(f6324,plain,(
% 203.34/26.57 ~sK6_skl(sK5_skl,sK4_skl,sK10_skl)=host(sK5_skl)|leq(nbr_proc,host(sK10_skl))|~index(ldr,host(sK10_skl))=host(sK10_skl)|~index(status,host(sK10_skl))=norm|~sQ51_spl|~sQ39_spl),
% 203.34/26.57 inference(resolution,[status(thm)],[f6323,f238])).
% 203.34/26.57 fof(f6326,definition,(
% 203.34/26.57 sQ208_spl <=> (sK6_skl(sK5_skl,sK4_skl,sK10_skl)=host(sK5_skl))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6329,plain,(
% 203.34/26.57 ~sQ208_spl|sQ197_spl|~sQ21_spl|~sQ20_spl|~sQ51_spl|~sQ39_spl),
% 203.34/26.57 inference(split_clause,[status(thm)],[f6324,f6326,f6120,f391,f388,f989,f835])).
% 203.34/26.57 fof(f6410,plain,(
% 203.34/26.57 ![X0,X1,X2]: (leq(X0,s(X1))|leq(X2,X0)|leq(X1,X2))),
% 203.34/26.57 inference(resolution,[status(thm)],[f3513,f5220])).
% 203.34/26.57 fof(f6575,plain,(
% 203.34/26.57 ![X0,X1]: (leq(zero,s(X0))|leq(X0,host(X1)))),
% 203.34/26.57 inference(resolution,[status(thm)],[f6410,f1032])).
% 203.34/26.57 fof(f6662,definition,(
% 203.34/26.57 sQ210_spl <=> (leq(s(nbr_proc),nbr_proc))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6663,plain,(
% 203.34/26.57 leq(s(nbr_proc),nbr_proc)|~sQ210_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f6662])).
% 203.34/26.57 fof(f6667,definition,(
% 203.34/26.57 sQ211_spl <=> (leq(s(host(sK5_skl)),host(sK5_skl)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6668,plain,(
% 203.34/26.57 leq(s(host(sK5_skl)),host(sK5_skl))|~sQ211_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f6667])).
% 203.34/26.57 fof(f6681,plain,(
% 203.34/26.57 $false|~sQ211_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f6668,f191])).
% 203.34/26.57 fof(f6682,plain,(
% 203.34/26.57 ~sQ211_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f6681])).
% 203.34/26.57 fof(f6749,definition,(
% 203.34/26.57 ![X0]: (sQ216_spl <=> (leq(zero,s(host(X0)))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6896,definition,(
% 203.34/26.57 sQ222_spl <=> (leq(host(sK10_skl),host(sK10_skl)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6898,plain,(
% 203.34/26.57 ~leq(host(sK10_skl),host(sK10_skl))|sQ222_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f6896])).
% 203.34/26.57 fof(f6942,definition,(
% 203.34/26.57 sQ223_spl <=> (host(sK10_skl)=s(nbr_proc))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f6943,plain,(
% 203.34/26.57 host(sK10_skl)=s(nbr_proc)|~sQ223_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f6942])).
% 203.34/26.57 fof(f6967,plain,(
% 203.34/26.57 $false|sQ192_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f5494,f192])).
% 203.34/26.57 fof(f6968,plain,(
% 203.34/26.57 sQ192_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f6967])).
% 203.34/26.57 fof(f7055,plain,(
% 203.34/26.57 ~leq(host(sK10_skl),nbr_proc)|~sQ223_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f6943,f191])).
% 203.34/26.57 fof(f7093,plain,(
% 203.34/26.57 $false|~sQ223_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f7055,f76])).
% 203.34/26.57 fof(f7094,plain,(
% 203.34/26.57 ~sQ223_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f7093])).
% 203.34/26.57 fof(f7170,definition,(
% 203.34/26.57 sQ233_spl <=> (host(sK10_skl)=s(s(nbr_proc)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f7171,plain,(
% 203.34/26.57 host(sK10_skl)=s(s(nbr_proc))|~sQ233_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f7170])).
% 203.34/26.57 fof(f7216,plain,(
% 203.34/26.57 ~leq(host(sK10_skl),nbr_proc)|~sQ233_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f7171,f295])).
% 203.34/26.57 fof(f7291,plain,(
% 203.34/26.57 $false|~sQ233_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f7216,f76])).
% 203.34/26.57 fof(f7292,plain,(
% 203.34/26.57 ~sQ233_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f7291])).
% 203.34/26.57 fof(f7413,definition,(
% 203.34/26.57 ![X0]: (sQ240_spl <=> (leq(s(nbr_proc),host(X0))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f7414,plain,(
% 203.34/26.57 ![X0]: (leq(s(nbr_proc),host(X0))|~sQ240_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f7413])).
% 203.34/26.57 fof(f8098,definition,(
% 203.34/26.57 sQ251_spl <=> (host(sK10_skl)=s(s(s(nbr_proc))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f8099,plain,(
% 203.34/26.57 host(sK10_skl)=s(s(s(nbr_proc)))|~sQ251_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f8098])).
% 203.34/26.57 fof(f8141,plain,(
% 203.34/26.57 ~leq(host(sK10_skl),nbr_proc)|~sQ251_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f8099,f329])).
% 203.34/26.57 fof(f8231,plain,(
% 203.34/26.57 $false|~sQ251_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f8141,f76])).
% 203.34/26.57 fof(f8232,plain,(
% 203.34/26.57 ~sQ251_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f8231])).
% 203.34/26.57 fof(f8298,definition,(
% 203.34/26.57 sQ258_spl <=> (setIn(sK10_skl,alive))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f8300,plain,(
% 203.34/26.57 ~setIn(sK10_skl,alive)|sQ258_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f8298])).
% 203.34/26.57 fof(f8463,plain,(
% 203.34/26.57 ![X0]: (~s(host(X0))=host(X0))),
% 203.34/26.57 inference(equality_resolution,[status(thm)],[f73])).
% 203.34/26.57 fof(f8608,definition,(
% 203.34/26.57 sQ259_spl <=> (leq(s(s(nbr_proc)),s(nbr_proc)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f8609,plain,(
% 203.34/26.57 leq(s(s(nbr_proc)),s(nbr_proc))|~sQ259_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f8608])).
% 203.34/26.57 fof(f8612,definition,(
% 203.34/26.57 sQ260_spl <=> (leq(s(s(nbr_proc)),nbr_proc))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f8613,plain,(
% 203.34/26.57 leq(s(s(nbr_proc)),nbr_proc)|~sQ260_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f8612])).
% 203.34/26.57 fof(f8619,definition,(
% 203.34/26.57 ![X0]: (sQ262_spl <=> (leq(s(s(nbr_proc)),host(X0))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f8620,plain,(
% 203.34/26.57 ![X0]: (leq(s(s(nbr_proc)),host(X0))|~sQ262_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f8619])).
% 203.34/26.57 fof(f8638,plain,(
% 203.34/26.57 $false|~sQ210_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f6663,f191])).
% 203.34/26.57 fof(f8639,plain,(
% 203.34/26.57 ~sQ210_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f8638])).
% 203.34/26.57 fof(f8688,plain,(
% 203.34/26.57 ![X0]: (~leq(host(X0),nbr_proc)|~sQ262_spl)),
% 203.34/26.57 inference(resolution,[status(thm)],[f8620,f1014])).
% 203.34/26.57 fof(f8706,plain,(
% 203.34/26.57 $false|~sQ262_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f8688,f76])).
% 203.34/26.57 fof(f8707,plain,(
% 203.34/26.57 ~sQ262_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f8706])).
% 203.34/26.57 fof(f9185,definition,(
% 203.34/26.57 ![X0]: (sQ294_spl <=> (leq(host(X0),zero)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f9186,plain,(
% 203.34/26.57 ![X0]: (leq(host(X0),zero)|~sQ294_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f9185])).
% 203.34/26.57 fof(f9230,plain,(
% 203.34/26.57 $false|~sQ294_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f9186,f1032])).
% 203.34/26.57 fof(f9231,plain,(
% 203.34/26.57 ~sQ294_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f9230])).
% 203.34/26.57 fof(f9246,plain,(
% 203.34/26.57 $false|~sQ260_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f8613,f295])).
% 203.34/26.57 fof(f9247,plain,(
% 203.34/26.57 ~sQ260_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f9246])).
% 203.34/26.57 fof(f9248,plain,(
% 203.34/26.57 $false|~sQ259_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f8609,f191])).
% 203.34/26.57 fof(f9249,plain,(
% 203.34/26.57 ~sQ259_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f9248])).
% 203.34/26.57 fof(f9250,plain,(
% 203.34/26.57 $false|sQ258_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f8300,f238])).
% 203.34/26.57 fof(f9251,plain,(
% 203.34/26.57 sQ258_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f9250])).
% 203.34/26.57 fof(f9266,plain,(
% 203.34/26.57 $false|sQ87_spl),
% 203.34/26.57 inference(trivial_equality_resolution,[status(thm)],[f2241])).
% 203.34/26.57 fof(f9267,plain,(
% 203.34/26.57 sQ87_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f9266])).
% 203.34/26.57 fof(f9795,definition,(
% 203.34/26.57 sQ323_spl <=> (leq(host(sK4_skl),host(sK4_skl)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f9797,plain,(
% 203.34/26.57 ~leq(host(sK4_skl),host(sK4_skl))|sQ323_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f9795])).
% 203.34/26.57 fof(f9800,plain,(
% 203.34/26.57 $false|sQ323_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f9797,f192])).
% 203.34/26.57 fof(f9801,plain,(
% 203.34/26.57 sQ323_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f9800])).
% 203.34/26.57 fof(f9808,plain,(
% 203.34/26.57 ![X0]: (~leq(host(X0),nbr_proc)|~sQ240_spl)),
% 203.34/26.57 inference(resolution,[status(thm)],[f7414,f1020])).
% 203.34/26.57 fof(f9819,plain,(
% 203.34/26.57 $false|~sQ240_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f9808,f76])).
% 203.34/26.57 fof(f9820,plain,(
% 203.34/26.57 ~sQ240_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f9819])).
% 203.34/26.57 fof(f12369,definition,(
% 203.34/26.57 sQ369_spl <=> (host(sK5_skl)=s(host(sK5_skl)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f12370,plain,(
% 203.34/26.57 host(sK5_skl)=s(host(sK5_skl))|~sQ369_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f12369])).
% 203.34/26.57 fof(f12381,plain,(
% 203.34/26.57 $false|~sQ369_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f12370,f8463])).
% 203.34/26.57 fof(f12382,plain,(
% 203.34/26.57 ~sQ369_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f12381])).
% 203.34/26.57 fof(f12823,definition,(
% 203.34/26.57 ![X0]: (sQ376_spl <=> (q_nil=cons(X0,init(q_nil))))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f12824,plain,(
% 203.34/26.57 ![X0]: (q_nil=cons(X0,init(q_nil))|~sQ376_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f12823])).
% 203.34/26.57 fof(f12842,plain,(
% 203.34/26.57 $false|~sQ376_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f12824,f133])).
% 203.34/26.57 fof(f12843,plain,(
% 203.34/26.57 ~sQ376_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f12842])).
% 203.34/26.57 fof(f12915,definition,(
% 203.34/26.57 sQ378_spl <=> (nbr_proc=nbr_proc)),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f12917,plain,(
% 203.34/26.57 ~nbr_proc=nbr_proc|sQ378_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f12915])).
% 203.34/26.57 fof(f12919,plain,(
% 203.34/26.57 $false|sQ378_spl),
% 203.34/26.57 inference(trivial_equality_resolution,[status(thm)],[f12917])).
% 203.34/26.57 fof(f12920,plain,(
% 203.34/26.57 sQ378_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f12919])).
% 203.34/26.57 fof(f13306,plain,(
% 203.34/26.57 ![X0]: (leq(s(zero),sK6_skl(sK5_skl,sK4_skl,X0))|leq(nbr_proc,host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ51_spl|~sQ31_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f990,f580])).
% 203.34/26.57 fof(f13356,plain,(
% 203.34/26.57 ![X0,X1]: (~leq(host(X0),X1)|leq(zero,s(X1)))),
% 203.34/26.57 inference(resolution,[status(thm)],[f74,f1018])).
% 203.34/26.57 fof(f13391,plain,(
% 203.34/26.57 $false|sQ173_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f4470,f192])).
% 203.34/26.57 fof(f13392,plain,(
% 203.34/26.57 sQ173_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f13391])).
% 203.34/26.57 fof(f14090,definition,(
% 203.34/26.57 sQ399_spl <=> (leq(s(zero),zero))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f14091,plain,(
% 203.34/26.57 leq(s(zero),zero)|~sQ399_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f14090])).
% 203.34/26.57 fof(f14095,plain,(
% 203.34/26.57 $false|~sQ399_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f14091,f191])).
% 203.34/26.57 fof(f14096,plain,(
% 203.34/26.57 ~sQ399_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f14095])).
% 203.34/26.57 fof(f15785,definition,(
% 203.34/26.57 ![X0]: (sQ417_spl <=> (~leq(host(X0),nbr_proc)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f15786,plain,(
% 203.34/26.57 ![X0]: (~leq(host(X0),nbr_proc)|~sQ417_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f15785])).
% 203.34/26.57 fof(f15810,plain,(
% 203.34/26.57 $false|~sQ417_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f15786,f76])).
% 203.34/26.57 fof(f15811,plain,(
% 203.34/26.57 ~sQ417_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f15810])).
% 203.34/26.57 fof(f16712,definition,(
% 203.34/26.57 sQ434_spl <=> (nbr_proc=s(s(nbr_proc)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f16713,plain,(
% 203.34/26.57 nbr_proc=s(s(nbr_proc))|~sQ434_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f16712])).
% 203.34/26.57 fof(f16718,definition,(
% 203.34/26.57 sQ435_spl <=> (nbr_proc=s(nbr_proc))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f16719,plain,(
% 203.34/26.57 nbr_proc=s(nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(component_clause,[status(thm)],[f16718])).
% 203.34/26.57 fof(f16793,plain,(
% 203.34/26.57 ~leq(s(s(s(s(s(s(s(s(s(nbr_proc))))))))),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(paramodulation,[status(thm)],[f16719,f614])).
% 203.34/26.57 fof(f16863,plain,(
% 203.34/26.57 ~leq(s(s(s(s(s(s(s(s(nbr_proc)))))))),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16793])).
% 203.34/26.57 fof(f16864,plain,(
% 203.34/26.57 ~leq(s(s(s(s(s(s(s(nbr_proc))))))),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16863])).
% 203.34/26.57 fof(f16865,plain,(
% 203.34/26.57 ~leq(s(s(s(s(s(s(nbr_proc)))))),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16864])).
% 203.34/26.57 fof(f16866,plain,(
% 203.34/26.57 ~leq(s(s(s(s(s(nbr_proc))))),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16865])).
% 203.34/26.57 fof(f16867,plain,(
% 203.34/26.57 ~leq(s(s(s(s(nbr_proc)))),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16866])).
% 203.34/26.57 fof(f16868,plain,(
% 203.34/26.57 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16867])).
% 203.34/26.57 fof(f16869,plain,(
% 203.34/26.57 ~leq(s(s(nbr_proc)),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16868])).
% 203.34/26.57 fof(f16870,plain,(
% 203.34/26.57 ~leq(s(nbr_proc),nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16869])).
% 203.34/26.57 fof(f16871,plain,(
% 203.34/26.57 ~leq(nbr_proc,nbr_proc)|~sQ435_spl),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f16719,f16870])).
% 203.34/26.57 fof(f16872,plain,(
% 203.34/26.57 $false|~sQ435_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f16871,f192])).
% 203.34/26.57 fof(f16873,plain,(
% 203.34/26.57 ~sQ435_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f16872])).
% 203.34/26.57 fof(f17705,plain,(
% 203.34/26.57 $false|~sQ165_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f4247,f76])).
% 203.34/26.57 fof(f17706,plain,(
% 203.34/26.57 ~sQ165_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f17705])).
% 203.34/26.57 fof(f19428,definition,(
% 203.34/26.57 ![X0]: (sQ483_spl <=> (tail(cons(X0,q_nil))=snoc(tail(q_nil),X0)))),
% 203.34/26.57 introduced(definition,[new_symbols(definition,[sQ483_spl])],[split_symbol_definition])).
% 203.34/26.57 fof(f19429,plain,(
% 203.34/26.57 ![X0]: (tail(cons(X0,q_nil))=snoc(tail(q_nil),X0)|~sQ483_spl)),
% 203.34/26.57 inference(component_clause,[status(thm)],[f19428])).
% 203.34/26.57 fof(f19946,plain,(
% 203.34/26.57 ![X0]: (q_nil=snoc(tail(q_nil),X0)|~sQ483_spl)),
% 203.34/26.57 inference(forward_demodulation,[status(thm)],[f128,f19429])).
% 203.34/26.57 fof(f19947,plain,(
% 203.34/26.57 $false|~sQ483_spl),
% 203.34/26.57 inference(forward_subsumption_resolution,[status(thm)],[f19946,f134])).
% 203.34/26.57 fof(f19948,plain,(
% 203.34/26.57 ~sQ483_spl),
% 203.34/26.57 inference(contradiction_clause,[status(thm)],[f19947])).
% 203.34/26.57 fof(f20087,definition,(
% 203.34/26.57 ![X0]: (sQ505_spl <=> (~leq(host(X0),host(sK10_skl))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ505_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f20088,plain,(
% 203.34/26.59 ![X0]: (~leq(host(X0),host(sK10_skl))|~sQ505_spl)),
% 203.34/26.59 inference(component_clause,[status(thm)],[f20087])).
% 203.34/26.59 fof(f20208,definition,(
% 203.34/26.59 ![X0]: (sQ507_spl <=> (~leq(host(X0),host(sK5_skl))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ507_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f20209,plain,(
% 203.34/26.59 ![X0]: (~leq(host(X0),host(sK5_skl))|~sQ507_spl)),
% 203.34/26.59 inference(component_clause,[status(thm)],[f20208])).
% 203.34/26.59 fof(f20388,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(s(s(nbr_proc)))))))),nbr_proc)|~sQ434_spl),
% 203.34/26.59 inference(paramodulation,[status(thm)],[f16713,f614])).
% 203.34/26.59 fof(f20485,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(nbr_proc)))))),nbr_proc)|~sQ434_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f16713,f20388])).
% 203.34/26.59 fof(f20486,plain,(
% 203.34/26.59 ~leq(s(s(s(s(nbr_proc)))),nbr_proc)|~sQ434_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f16713,f20485])).
% 203.34/26.59 fof(f20487,plain,(
% 203.34/26.59 ~leq(s(s(nbr_proc)),nbr_proc)|~sQ434_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f16713,f20486])).
% 203.34/26.59 fof(f20488,plain,(
% 203.34/26.59 ~leq(nbr_proc,nbr_proc)|~sQ434_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f16713,f20487])).
% 203.34/26.59 fof(f20489,plain,(
% 203.34/26.59 $false|~sQ434_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f20488,f192])).
% 203.34/26.59 fof(f20490,plain,(
% 203.34/26.59 ~sQ434_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f20489])).
% 203.34/26.59 fof(f20651,plain,(
% 203.34/26.59 $false|~sQ505_spl),
% 203.34/26.59 inference(resolution,[status(thm)],[f20088,f193])).
% 203.34/26.59 fof(f20657,plain,(
% 203.34/26.59 ~sQ505_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f20651])).
% 203.34/26.59 fof(f20679,plain,(
% 203.34/26.59 $false|~sQ507_spl),
% 203.34/26.59 inference(resolution,[status(thm)],[f20209,f193])).
% 203.34/26.59 fof(f20685,plain,(
% 203.34/26.59 ~sQ507_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f20679])).
% 203.34/26.59 fof(f24327,plain,(
% 203.34/26.59 ![X0,X1]: (leq(zero,s(host(X0)))|leq(zero,s(host(X1))))),
% 203.34/26.59 inference(resolution,[status(thm)],[f13356,f6575])).
% 203.34/26.59 fof(f24358,plain,(
% 203.34/26.59 sQ216_spl),
% 203.34/26.59 inference(split_clause,[status(thm)],[f24327,f6749])).
% 203.34/26.59 fof(f26725,plain,(
% 203.34/26.59 $false|sQ169_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f4400,f192])).
% 203.34/26.59 fof(f26726,plain,(
% 203.34/26.59 sQ169_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f26725])).
% 203.34/26.59 fof(f27121,definition,(
% 203.34/26.59 sQ604_spl <=> (leq(nbr_proc,s(s(nbr_proc))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f27123,plain,(
% 203.34/26.59 ~leq(nbr_proc,s(s(nbr_proc)))|sQ604_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f27121])).
% 203.34/26.59 fof(f27152,plain,(
% 203.34/26.59 $false|sQ604_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f27123,f359])).
% 203.34/26.59 fof(f27153,plain,(
% 203.34/26.59 sQ604_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f27152])).
% 203.34/26.59 fof(f27598,definition,(
% 203.34/26.59 ![X0]: (sQ609_spl <=> (~leq(host(sK5_skl),host(X0))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f27599,plain,(
% 203.34/26.59 ![X0]: (~leq(host(sK5_skl),host(X0))|~sQ609_spl)),
% 203.34/26.59 inference(component_clause,[status(thm)],[f27598])).
% 203.34/26.59 fof(f27739,plain,(
% 203.34/26.59 $false|~sQ609_spl),
% 203.34/26.59 inference(resolution,[status(thm)],[f27599,f193])).
% 203.34/26.59 fof(f27745,plain,(
% 203.34/26.59 ~sQ609_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f27739])).
% 203.34/26.59 fof(f27874,definition,(
% 203.34/26.59 sQ615_spl <=> (s(nbr_proc)=s(s(s(s(nbr_proc)))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f27875,plain,(
% 203.34/26.59 s(nbr_proc)=s(s(s(s(nbr_proc))))|~sQ615_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f27874])).
% 203.34/26.59 fof(f27878,definition,(
% 203.34/26.59 sQ616_spl <=> (s(nbr_proc)=s(s(s(nbr_proc))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f27879,plain,(
% 203.34/26.59 s(nbr_proc)=s(s(s(nbr_proc)))|~sQ616_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f27878])).
% 203.34/26.59 fof(f27882,definition,(
% 203.34/26.59 sQ617_spl <=> (nbr_proc=s(s(s(nbr_proc))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f27883,plain,(
% 203.34/26.59 nbr_proc=s(s(s(nbr_proc)))|~sQ617_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f27882])).
% 203.34/26.59 fof(f27918,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(nbr_proc)))))),nbr_proc)|~sQ617_spl),
% 203.34/26.59 inference(paramodulation,[status(thm)],[f27883,f585])).
% 203.34/26.59 fof(f28039,plain,(
% 203.34/26.59 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ617_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27883,f27918])).
% 203.34/26.59 fof(f28040,plain,(
% 203.34/26.59 ~leq(nbr_proc,nbr_proc)|~sQ617_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27883,f28039])).
% 203.34/26.59 fof(f28041,plain,(
% 203.34/26.59 $false|~sQ617_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f28040,f192])).
% 203.34/26.59 fof(f28042,plain,(
% 203.34/26.59 ~sQ617_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f28041])).
% 203.34/26.59 fof(f28113,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(s(s(s(nbr_proc))))))))),s(nbr_proc))|~sQ616_spl),
% 203.34/26.59 inference(paramodulation,[status(thm)],[f27879,f614])).
% 203.34/26.59 fof(f28225,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(s(nbr_proc))))))),s(nbr_proc))|~sQ616_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27879,f28113])).
% 203.34/26.59 fof(f28226,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(nbr_proc))))),s(nbr_proc))|~sQ616_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27879,f28225])).
% 203.34/26.59 fof(f28227,plain,(
% 203.34/26.59 ~leq(s(s(s(nbr_proc))),s(nbr_proc))|~sQ616_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27879,f28226])).
% 203.34/26.59 fof(f28228,plain,(
% 203.34/26.59 ~leq(s(nbr_proc),s(nbr_proc))|~sQ616_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27879,f28227])).
% 203.34/26.59 fof(f28229,plain,(
% 203.34/26.59 $false|~sQ616_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f28228,f192])).
% 203.34/26.59 fof(f28230,plain,(
% 203.34/26.59 ~sQ616_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f28229])).
% 203.34/26.59 fof(f29141,plain,(
% 203.34/26.59 ![X0]: (X0=m_Halt(sK0_skl(X0))|X0=m_Down(sK1_skl(X0))|~sQ187_spl)),
% 203.34/26.59 inference(backward_subsumption_resolution,[status(thm)],[f151,f5038])).
% 203.34/26.59 fof(f29196,plain,(
% 203.34/26.59 ![X0,X1]: (m_Ack(X0,X1)=m_Halt(sK0_skl(m_Ack(X0,X1)))|~sQ187_spl)),
% 203.34/26.59 inference(resolution,[status(thm)],[f29141,f84])).
% 203.34/26.59 fof(f29221,plain,(
% 203.34/26.59 $false|~sQ187_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f29196,f83])).
% 203.34/26.59 fof(f29222,plain,(
% 203.34/26.59 ~sQ187_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f29221])).
% 203.34/26.59 fof(f29260,definition,(
% 203.34/26.59 sQ631_spl <=> (host(pidMsg(m_Down(sK5_skl)))=host(sK5_skl))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ631_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f29262,plain,(
% 203.34/26.59 ~host(pidMsg(m_Down(sK5_skl)))=host(sK5_skl)|sQ631_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f29260])).
% 203.34/26.59 fof(f29324,plain,(
% 203.34/26.59 ~host(sK5_skl)=host(sK5_skl)|sQ631_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f155,f29262])).
% 203.34/26.59 fof(f29325,plain,(
% 203.34/26.59 $false|sQ631_spl),
% 203.34/26.59 inference(trivial_equality_resolution,[status(thm)],[f29324])).
% 203.34/26.59 fof(f29326,plain,(
% 203.34/26.59 sQ631_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f29325])).
% 203.34/26.59 fof(f29987,plain,(
% 203.34/26.59 $false|sQ177_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f4657,f357])).
% 203.34/26.59 fof(f29988,plain,(
% 203.34/26.59 sQ177_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f29987])).
% 203.34/26.59 fof(f30102,definition,(
% 203.34/26.59 sQ676_spl <=> (s(zero)=s(s(s(zero))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f30103,plain,(
% 203.34/26.59 s(zero)=s(s(s(zero)))|~sQ676_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f30102])).
% 203.34/26.59 fof(f30109,definition,(
% 203.34/26.59 sQ678_spl <=> (zero=s(s(s(zero))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ678_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f30110,plain,(
% 203.34/26.59 zero=s(s(s(zero)))|~sQ678_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f30109])).
% 203.34/26.59 fof(f30143,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(zero)))))),zero)|~sQ678_spl),
% 203.34/26.59 inference(paramodulation,[status(thm)],[f30110,f585])).
% 203.34/26.59 fof(f30267,plain,(
% 203.34/26.59 ~leq(s(s(s(zero))),zero)|~sQ678_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f30110,f30143])).
% 203.34/26.59 fof(f30268,plain,(
% 203.34/26.59 ~leq(zero,zero)|~sQ678_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f30110,f30267])).
% 203.34/26.59 fof(f30269,plain,(
% 203.34/26.59 $false|~sQ678_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f30268,f192])).
% 203.34/26.59 fof(f30270,plain,(
% 203.34/26.59 ~sQ678_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f30269])).
% 203.34/26.59 fof(f30294,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(s(s(s(zero))))))))),s(zero))|~sQ676_spl),
% 203.34/26.59 inference(paramodulation,[status(thm)],[f30103,f614])).
% 203.34/26.59 fof(f30409,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(s(zero))))))),s(zero))|~sQ676_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f30103,f30294])).
% 203.34/26.59 fof(f30410,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(zero))))),s(zero))|~sQ676_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f30103,f30409])).
% 203.34/26.59 fof(f30411,plain,(
% 203.34/26.59 ~leq(s(s(s(zero))),s(zero))|~sQ676_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f30103,f30410])).
% 203.34/26.59 fof(f30412,plain,(
% 203.34/26.59 ~leq(s(zero),s(zero))|~sQ676_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f30103,f30411])).
% 203.34/26.59 fof(f30413,plain,(
% 203.34/26.59 $false|~sQ676_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f30412,f192])).
% 203.34/26.59 fof(f30414,plain,(
% 203.34/26.59 ~sQ676_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f30413])).
% 203.34/26.59 fof(f31541,plain,(
% 203.34/26.59 $false|sQ191_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f5395,f192])).
% 203.34/26.59 fof(f31542,plain,(
% 203.34/26.59 sQ191_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f31541])).
% 203.34/26.59 fof(f34158,plain,(
% 203.34/26.59 ~leq(s(s(s(s(s(s(s(nbr_proc))))))),s(nbr_proc))|~sQ615_spl),
% 203.34/26.59 inference(paramodulation,[status(thm)],[f27875,f585])).
% 203.34/26.59 fof(f34289,plain,(
% 203.34/26.59 ~leq(s(s(s(s(nbr_proc)))),s(nbr_proc))|~sQ615_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27875,f34158])).
% 203.34/26.59 fof(f34290,plain,(
% 203.34/26.59 ~leq(s(nbr_proc),s(nbr_proc))|~sQ615_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f27875,f34289])).
% 203.34/26.59 fof(f34291,plain,(
% 203.34/26.59 $false|~sQ615_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f34290,f192])).
% 203.34/26.59 fof(f34292,plain,(
% 203.34/26.59 ~sQ615_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f34291])).
% 203.34/26.59 fof(f35448,plain,(
% 203.34/26.59 $false|sQ222_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f6898,f192])).
% 203.34/26.59 fof(f35449,plain,(
% 203.34/26.59 sQ222_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f35448])).
% 203.34/26.59 fof(f35450,plain,(
% 203.34/26.59 $false|~sQ203_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f6172,f76])).
% 203.34/26.59 fof(f35451,plain,(
% 203.34/26.59 ~sQ203_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f35450])).
% 203.34/26.59 fof(f37685,definition,(
% 203.34/26.59 sQ823_spl <=> (leq(s(zero),host(sK10_skl)))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ823_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f37687,plain,(
% 203.34/26.59 ~leq(s(zero),host(sK10_skl))|sQ823_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f37685])).
% 203.34/26.59 fof(f37702,plain,(
% 203.34/26.59 $false|sQ823_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f37687,f74])).
% 203.34/26.59 fof(f37703,plain,(
% 203.34/26.59 sQ823_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f37702])).
% 203.34/26.59 fof(f39595,definition,(
% 203.34/26.59 sQ860_spl <=> (zero=s(s(s(s(zero)))))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ860_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f39596,plain,(
% 203.34/26.59 zero=s(s(s(s(zero))))|~sQ860_spl),
% 203.34/26.59 inference(component_clause,[status(thm)],[f39595])).
% 203.34/26.59 fof(f39692,plain,(
% 203.34/26.59 ~leq(s(s(s(s(zero)))),zero)|~sQ860_spl),
% 203.34/26.59 inference(paramodulation,[status(thm)],[f39596,f503])).
% 203.34/26.59 fof(f39830,plain,(
% 203.34/26.59 ~leq(zero,zero)|~sQ860_spl),
% 203.34/26.59 inference(forward_demodulation,[status(thm)],[f39596,f39692])).
% 203.34/26.59 fof(f39831,plain,(
% 203.34/26.59 $false|~sQ860_spl),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f39830,f192])).
% 203.34/26.59 fof(f39832,plain,(
% 203.34/26.59 ~sQ860_spl),
% 203.34/26.59 inference(contradiction_clause,[status(thm)],[f39831])).
% 203.34/26.59 fof(f40165,plain,(
% 203.34/26.59 ![X0]: (~leq(s(zero),sK6_skl(sK5_skl,sK4_skl,X0))|sK6_skl(sK5_skl,sK4_skl,X0)=host(sK5_skl)|leq(nbr_proc,host(X0))|~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ30_spl|~sQ57_spl|~sQ51_spl)),
% 203.34/26.59 inference(forward_subsumption_resolution,[status(thm)],[f3464,f6114])).
% 203.34/26.59 fof(f40166,plain,(
% 203.34/26.59 ~leq(s(zero),sK6_skl(sK5_skl,sK4_skl,sK10_skl))|sK6_skl(sK5_skl,sK4_skl,sK10_skl)=host(sK5_skl)|leq(nbr_proc,host(sK10_skl))|~index(ldr,host(sK10_skl))=host(sK10_skl)|~index(status,host(sK10_skl))=norm|~sQ30_spl|~sQ57_spl|~sQ51_spl),
% 203.34/26.59 inference(resolution,[status(thm)],[f40165,f238])).
% 203.34/26.59 fof(f40168,definition,(
% 203.34/26.59 sQ869_spl <=> (leq(s(zero),sK6_skl(sK5_skl,sK4_skl,sK10_skl)))),
% 203.34/26.59 introduced(definition,[new_symbols(definition,[sQ869_spl])],[split_symbol_definition])).
% 203.34/26.59 fof(f40171,plain,(
% 203.34/26.59 ~sQ869_spl|sQ208_spl|sQ197_spl|~sQ21_spl|~sQ20_spl|~sQ30_spl|~sQ57_spl|~sQ51_spl),
% 203.34/26.59 inference(split_clause,[status(thm)],[f40166,f40168,f6326,f6120,f391,f388,f558,f1142,f989])).
% 130.15/26.67 fof(f40928,definition,(
% 130.15/26.67 sQ876_spl <=> (leq(s(s(nbr_proc)),s(s(nbr_proc))))),
% 130.15/26.67 introduced(definition,[new_symbols(definition,[sQ876_spl])],[split_symbol_definition])).
% 130.15/26.67 fof(f40930,plain,(
% 130.15/26.67 ~leq(s(s(nbr_proc)),s(s(nbr_proc)))|sQ876_spl),
% 130.15/26.67 inference(component_clause,[status(thm)],[f40928])).
% 130.15/26.67 fof(f40958,plain,(
% 130.15/26.67 $false|sQ876_spl),
% 130.15/26.67 inference(forward_subsumption_resolution,[status(thm)],[f40930,f192])).
% 130.15/26.67 fof(f40959,plain,(
% 130.15/26.67 sQ876_spl),
% 130.15/26.67 inference(contradiction_clause,[status(thm)],[f40958])).
% 130.15/26.67 fof(f41574,definition,(
% 130.15/26.67 sQ883_spl <=> (nbr_proc=s(s(s(s(nbr_proc)))))),
% 130.15/26.67 introduced(definition,[new_symbols(definition,[sQ883_spl])],[split_symbol_definition])).
% 130.15/26.67 fof(f41575,plain,(
% 130.15/26.67 nbr_proc=s(s(s(s(nbr_proc))))|~sQ883_spl),
% 130.15/26.67 inference(component_clause,[status(thm)],[f41574])).
% 130.15/26.67 fof(f41609,plain,(
% 130.15/26.67 ~leq(s(s(s(s(nbr_proc)))),nbr_proc)|~sQ883_spl),
% 130.15/26.67 inference(paramodulation,[status(thm)],[f41575,f503])).
% 130.15/26.67 fof(f41753,plain,(
% 130.15/26.67 ~leq(nbr_proc,nbr_proc)|~sQ883_spl),
% 130.15/26.67 inference(forward_demodulation,[status(thm)],[f41575,f41609])).
% 130.15/26.67 fof(f41754,plain,(
% 130.15/26.67 $false|~sQ883_spl),
% 130.15/26.67 inference(forward_subsumption_resolution,[status(thm)],[f41753,f192])).
% 130.15/26.67 fof(f41755,plain,(
% 130.15/26.67 ~sQ883_spl),
% 130.15/26.67 inference(contradiction_clause,[status(thm)],[f41754])).
% 130.15/26.67 fof(f41978,plain,(
% 130.15/26.67 leq(s(zero),sK6_skl(sK5_skl,sK4_skl,sK10_skl))|leq(nbr_proc,host(sK10_skl))|~index(ldr,host(sK10_skl))=host(sK10_skl)|~index(status,host(sK10_skl))=norm|~sQ51_spl|~sQ31_spl),
% 130.15/26.67 inference(resolution,[status(thm)],[f13306,f238])).
% 130.15/26.67 fof(f41981,plain,(
% 130.15/26.67 sQ869_spl|sQ197_spl|~sQ21_spl|~sQ20_spl|~sQ51_spl|~sQ31_spl),
% 130.15/26.67 inference(split_clause,[status(thm)],[f41978,f40168,f6120,f391,f388,f989,f579])).
% 130.15/26.67 fof(f41983,plain,(
% 130.15/26.67 $false),
% 130.15/26.67 inference(sat_refutation,[status(thm)],[f322,f405,f561,f582,f838,f992,f1005,f1145,f1219,f2443,f2676,f3074,f3376,f3387,f3710,f6296,f6329,f6682,f6968,f7094,f7292,f8232,f8639,f8707,f9231,f9247,f9249,f9251,f9267,f9801,f9820,f12382,f12843,f12920,f13392,f14096,f15811,f16873,f17706,f19948,f20490,f20657,f20685,f24358,f26726,f27153,f27745,f28042,f28230,f29222,f29326,f29988,f30270,f30414,f31542,f34292,f35449,f35451,f37703,f39832,f40171,f40959,f41755,f41981])).
% 130.15/26.67 % SZS output end CNFRefutation for theBenchmark.p
% 130.15/26.70 % Elapsed time: 25.923312 seconds
% 130.15/26.70 % CPU time: 204.402139 seconds
% 130.15/26.70 % Total memory used: 605.257 MB
% 130.15/26.70 % Net memory used: 505.594 MB
%------------------------------------------------------------------------------