%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV465+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 : n017.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 98.39s 12.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV465+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.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:47:57 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 98.39/12.85 % Refutation found
% 98.39/12.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 98.39/12.85 % SZS output start CNFRefutation for theBenchmark
% 98.39/12.85 fof(f2,axiom,(
% 98.39/12.85 (! [P,Q] :( s(host(P)) = host(Q)=> host(P) != host(Q) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f3,axiom,(
% 98.39/12.85 (! [P] : leq(s(zero),host(P)) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f4,axiom,(
% 98.39/12.85 leq(s(zero),nbr_proc) ),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f5,axiom,(
% 98.39/12.85 (! [P] : leq(host(P),nbr_proc) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f14,axiom,(
% 98.39/12.85 (! [X,Y,Z] : m_Ack(X,Y) != m_NotNorm(Z) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f20,axiom,(
% 98.39/12.85 (! [X,Y] : m_Down(X) != m_NotNorm(Y) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f37,axiom,(
% 98.39/12.85 (! [X,Q] : tail(cons(X,Q)) = Q )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f42,axiom,(
% 98.39/12.85 (! [X,Q] : q_nil != cons(X,Q) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f43,axiom,(
% 98.39/12.85 (! [Y,Q] : q_nil != snoc(Q,Y) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f47,axiom,(
% 98.39/12.85 (! [X,Y,Q] :( elem(X,cons(Y,Q))<=> ( X = Y| elem(X,Q) ) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f48,axiom,(
% 98.39/12.85 (! [X,Y,Q] :( elem(X,snoc(Q,Y))<=> ( X = Y| elem(X,Q) ) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f59,axiom,(
% 98.39/12.85 (! [X] : ~ leq(s(X),X) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f60,axiom,(
% 98.39/12.85 (! [X] : leq(X,X) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f61,axiom,(
% 98.39/12.85 (! [X,Y] :( leq(X,Y)| leq(Y,X) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f62,axiom,(
% 98.39/12.85 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f63,axiom,(
% 98.39/12.85 (! [X,Y,Z] :( ( leq(X,Y)& leq(Y,Z) )=> leq(X,Z) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f64,axiom,(
% 98.39/12.85 (! [X,Y] :( leq(X,Y)<=> leq(s(X),s(Y)) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f65,axiom,(
% 98.39/12.85 (! [X,Y] :( leq(X,s(Y))<=> ( X = s(Y)| leq(X,Y) ) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f67,conjecture,(
% 98.39/12.85 (! [V,W,X] :( ( (! [Y,Z] :( elem(m_Ldr(Z),queue(host(Y)))=> ~ leq(host(Y),host(Z)) ))& (! [Y,Z] :( elem(m_Down(Z),queue(host(Y)))=> host(Z) != host(Y) ))& (! [Y,Z] :( elem(m_Halt(Z),queue(host(Y)))=> ~ leq(host(Y),host(Z)) ))& (! [Y,Z,Pid0] :( elem(m_Ack(Pid0,Y),queue(host(Z)))=> ~ leq(host(Y),host(Pid0)) ))& (! [Y,Z] :( ( Z != Y& host(Z) = host(Y) )=> ( ~ setIn(Y,alive)| ~ setIn(Z,alive) ) ))& (! [Y,Z] :( ( setIn(Z,alive)& elem(m_Ack(Z,Y),queue(host(Z))) )=> leq(host(Y),index(pendack,host(Z))) ))& (! [Y,Z] :( ( setIn(Z,alive)& index(status,host(Z)) = elec_1 )=> ~ elem(m_Ack(Z,Y),queue(host(Z))) ))& (! [Y] :( ( ( index(status,host(Y)) = elec_1| index(status,host(Y)) = elec_2 )& setIn(Y,alive) )=> index(elid,host(Y)) = Y ))& (! [Y,Z] :( ( ~ leq(host(Y),host(Z))& setIn(Y,alive)& setIn(Z,alive)& index(status,host(Y)) = elec_2& index(status,host(Z)) = elec_2 )=> leq(index(pendack,host(Z)),host(Y)) ))& (! [Y,Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& host(Z) = host(Y) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& (! [Y,Z,Pid0] :( ( setIn(Y,alive)& setIn(Pid0,alive)& host(Pid0) = host(Z)& index(status,host(Y)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Y,Z),queue(host(Y))) ))& (! [Y,Z] :( ( ~ leq(host(Y),host(Z))& setIn(Y,alive)& setIn(Z,alive)& index(status,host(Y)) = elec_2& index(status,host(Z)) = elec_2 )=> ~ leq(index(pendack,host(Y)),index(pendack,host(Z))) ))& (! [Y,Z,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Y))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Z)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& (! [Y,Z,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) = host(Z)& host(Pid0) = nbr_proc& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Y,alive)& elem(m_Down(Z),queue(host(Y))) ) ))& (! [Y,Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0)))& elem(m_Down(Pid20),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Z) = index(pendack,host(Pid0))& host(Pid20) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& queue(host(X)) = cons(m_NormQ(W),V) )=> ( setIn(X,alive)=> ( index(status,host(X)) != norm=> (! [Y,Z,X0,Y0] :( host(W) = host(Y0)=> ( host(X) = host(Y0)=> ( ( setIn(Y0,alive)& elem(m_Down(X0),snoc(V,m_NotNorm(W)))& elem(m_Ack(Y0,Z),snoc(V,m_NotNorm(W)))& leq(nbr_proc,s(index(pendack,host(Y0))))& index(status,host(Y0)) = elec_2& host(Z) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ) ) ) )) ) ) )),
% 98.39/12.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 98.39/12.85 fof(f68,negated_conjecture,(
% 98.39/12.85 ~((! [V,W,X] :( ( (! [Y,Z] :( elem(m_Ldr(Z),queue(host(Y)))=> ~ leq(host(Y),host(Z)) ))& (! [Y,Z] :( elem(m_Down(Z),queue(host(Y)))=> host(Z) != host(Y) ))& (! [Y,Z] :( elem(m_Halt(Z),queue(host(Y)))=> ~ leq(host(Y),host(Z)) ))& (! [Y,Z,Pid0] :( elem(m_Ack(Pid0,Y),queue(host(Z)))=> ~ leq(host(Y),host(Pid0)) ))& (! [Y,Z] :( ( Z != Y& host(Z) = host(Y) )=> ( ~ setIn(Y,alive)| ~ setIn(Z,alive) ) ))& (! [Y,Z] :( ( setIn(Z,alive)& elem(m_Ack(Z,Y),queue(host(Z))) )=> leq(host(Y),index(pendack,host(Z))) ))& (! [Y,Z] :( ( setIn(Z,alive)& index(status,host(Z)) = elec_1 )=> ~ elem(m_Ack(Z,Y),queue(host(Z))) ))& (! [Y] :( ( ( index(status,host(Y)) = elec_1| index(status,host(Y)) = elec_2 )& setIn(Y,alive) )=> index(elid,host(Y)) = Y ))& (! [Y,Z] :( ( ~ leq(host(Y),host(Z))& setIn(Y,alive)& setIn(Z,alive)& index(status,host(Y)) = elec_2& index(status,host(Z)) = elec_2 )=> leq(index(pendack,host(Z)),host(Y)) ))& (! [Y,Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Z),queue(host(Pid0)))& host(Z) = host(Y) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& (! [Y,Z,Pid0] :( ( setIn(Y,alive)& setIn(Pid0,alive)& host(Pid0) = host(Z)& index(status,host(Y)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Y,Z),queue(host(Y))) ))& (! [Y,Z] :( ( ~ leq(host(Y),host(Z))& setIn(Y,alive)& setIn(Z,alive)& index(status,host(Y)) = elec_2& index(status,host(Z)) = elec_2 )=> ~ leq(index(pendack,host(Y)),index(pendack,host(Z))) ))& (! [Y,Z,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Y))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Z)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& (! [Y,Z,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) = host(Z)& host(Pid0) = nbr_proc& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Y,alive)& elem(m_Down(Z),queue(host(Y))) ) ))& (! [Y,Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0)))& elem(m_Down(Pid20),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Z) = index(pendack,host(Pid0))& host(Pid20) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ))& queue(host(X)) = cons(m_NormQ(W),V) )=> ( setIn(X,alive)=> ( index(status,host(X)) != norm=> (! [Y,Z,X0,Y0] :( host(W) = host(Y0)=> ( host(X) = host(Y0)=> ( ( setIn(Y0,alive)& elem(m_Down(X0),snoc(V,m_NotNorm(W)))& elem(m_Ack(Y0,Z),snoc(V,m_NotNorm(W)))& leq(nbr_proc,s(index(pendack,host(Y0))))& index(status,host(Y0)) = elec_2& host(Z) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(Y,alive)& index(ldr,host(Y)) = host(Y)& index(status,host(Y)) = norm ) ) ) ) )) ) ) ))),
% 98.39/12.85 inference(negated_conjecture,[status(cth)],[f67])).
% 98.39/12.85 fof(f72,plain,(
% 98.39/12.85 ![P,Q]: (~s(host(P))=host(Q)|~host(P)=host(Q))),
% 98.39/12.85 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 98.39/12.85 fof(f73,plain,(
% 98.39/12.85 ![X0,X1]: (~s(host(X0))=host(X1)|~host(X0)=host(X1))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f72])).
% 98.39/12.85 fof(f74,plain,(
% 98.39/12.85 ![X0]: (leq(s(zero),host(X0)))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f3])).
% 98.39/12.85 fof(f75,plain,(
% 98.39/12.85 leq(s(zero),nbr_proc)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f4])).
% 98.39/12.85 fof(f76,plain,(
% 98.39/12.85 ![X0]: (leq(host(X0),nbr_proc))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f5])).
% 98.39/12.85 fof(f85,plain,(
% 98.39/12.85 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_NotNorm(X2))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f14])).
% 98.39/12.85 fof(f91,plain,(
% 98.39/12.85 ![X0,X1]: (~m_Down(X0)=m_NotNorm(X1))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f20])).
% 98.39/12.85 fof(f128,plain,(
% 98.39/12.85 ![X0,X1]: (tail(cons(X0,X1))=X1)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f37])).
% 98.39/12.85 fof(f133,plain,(
% 98.39/12.85 ![X0,X1]: (~q_nil=cons(X0,X1))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f42])).
% 98.39/12.85 fof(f134,plain,(
% 98.39/12.85 ![X0,X1]: (~q_nil=snoc(X0,X1))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f43])).
% 98.39/12.85 fof(f138,plain,(
% 98.39/12.85 ![X,Y,Q]: ((~elem(X,cons(Y,Q))|(X=Y|elem(X,Q)))&(elem(X,cons(Y,Q))|(~X=Y&~elem(X,Q))))),
% 98.39/12.85 inference(NNF_transformation,[status(thm)],[f47])).
% 98.39/12.85 fof(f139,plain,(
% 98.39/12.85 (![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))))),
% 98.39/12.85 inference(miniscoping,[status(thm)],[f138])).
% 98.39/12.85 fof(f142,plain,(
% 98.39/12.85 ![X0,X1,X2]: (elem(X0,cons(X1,X2))|~elem(X0,X2))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f139])).
% 98.39/12.85 fof(f143,plain,(
% 98.39/12.85 ![X,Y,Q]: ((~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q)))&(elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 98.39/12.85 inference(NNF_transformation,[status(thm)],[f48])).
% 98.39/12.85 fof(f144,plain,(
% 98.39/12.85 (![X,Y,Q]: (~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q))))&(![X,Y,Q]: (elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 98.39/12.85 inference(miniscoping,[status(thm)],[f143])).
% 98.39/12.85 fof(f145,plain,(
% 98.39/12.85 ![X0,X1,X2]: (~elem(X0,snoc(X1,X2))|X0=X2|elem(X0,X1))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f144])).
% 98.39/12.85 fof(f191,plain,(
% 98.39/12.85 ![X0]: (~leq(s(X0),X0))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f59])).
% 98.39/12.85 fof(f192,plain,(
% 98.39/12.85 ![X0]: (leq(X0,X0))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f60])).
% 98.39/12.85 fof(f193,plain,(
% 98.39/12.85 ![X0,X1]: (leq(X0,X1)|leq(X1,X0))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f61])).
% 98.39/12.85 fof(f194,plain,(
% 98.39/12.85 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 98.39/12.85 inference(NNF_transformation,[status(thm)],[f62])).
% 98.39/12.85 fof(f195,plain,(
% 98.39/12.85 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 98.39/12.85 inference(miniscoping,[status(thm)],[f194])).
% 98.39/12.85 fof(f196,plain,(
% 98.39/12.85 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f195])).
% 98.39/12.85 fof(f199,plain,(
% 98.39/12.85 ![X,Y,Z]: ((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))),
% 98.39/12.85 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 98.39/12.85 fof(f200,plain,(
% 98.39/12.85 ![X,Z]: ((![Y]: (~leq(X,Y)|~leq(Y,Z)))|leq(X,Z))),
% 98.39/12.85 inference(miniscoping,[status(thm)],[f199])).
% 98.39/12.85 fof(f201,plain,(
% 98.39/12.85 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f200])).
% 98.39/12.85 fof(f202,plain,(
% 98.39/12.85 ![X,Y]: ((~leq(X,Y)|leq(s(X),s(Y)))&(leq(X,Y)|~leq(s(X),s(Y))))),
% 98.39/12.85 inference(NNF_transformation,[status(thm)],[f64])).
% 98.39/12.85 fof(f203,plain,(
% 98.39/12.85 (![X,Y]: (~leq(X,Y)|leq(s(X),s(Y))))&(![X,Y]: (leq(X,Y)|~leq(s(X),s(Y))))),
% 98.39/12.85 inference(miniscoping,[status(thm)],[f202])).
% 98.39/12.85 fof(f204,plain,(
% 98.39/12.85 ![X0,X1]: (~leq(X0,X1)|leq(s(X0),s(X1)))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f203])).
% 98.39/12.85 fof(f205,plain,(
% 98.39/12.85 ![X0,X1]: (leq(X0,X1)|~leq(s(X0),s(X1)))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f203])).
% 98.39/12.85 fof(f206,plain,(
% 98.39/12.85 ![X,Y]: ((~leq(X,s(Y))|(X=s(Y)|leq(X,Y)))&(leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 98.39/12.85 inference(NNF_transformation,[status(thm)],[f65])).
% 98.39/12.85 fof(f207,plain,(
% 98.39/12.85 (![X,Y]: (~leq(X,s(Y))|(X=s(Y)|leq(X,Y))))&(![X,Y]: (leq(X,s(Y))|(~X=s(Y)&~leq(X,Y))))),
% 98.39/12.85 inference(miniscoping,[status(thm)],[f206])).
% 98.39/12.85 fof(f210,plain,(
% 98.39/12.85 ![X0,X1]: (leq(X0,s(X1))|~leq(X0,X1))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f207])).
% 98.39/12.85 fof(f212,plain,(
% 98.39/12.85 (?[V,W,X]: (((((((((((((((((![Y,Z]: (~elem(m_Ldr(Z),queue(host(Y)))|~leq(host(Y),host(Z))))&(![Y,Z]: (~elem(m_Down(Z),queue(host(Y)))|~host(Z)=host(Y))))&(![Y,Z]: (~elem(m_Halt(Z),queue(host(Y)))|~leq(host(Y),host(Z)))))&(![Y,Z,Pid0]: (~elem(m_Ack(Pid0,Y),queue(host(Z)))|~leq(host(Y),host(Pid0)))))&(![Y,Z]: ((Z=Y|~host(Z)=host(Y))|(~setIn(Y,alive)|~setIn(Z,alive)))))&(![Y,Z]: ((~setIn(Z,alive)|~elem(m_Ack(Z,Y),queue(host(Z))))|leq(host(Y),index(pendack,host(Z))))))&(![Y,Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|~elem(m_Ack(Z,Y),queue(host(Z))))))&(![Y]: (((~index(status,host(Y))=elec_1&~index(status,host(Y))=elec_2)|~setIn(Y,alive))|index(elid,host(Y))=Y)))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|leq(index(pendack,host(Z)),host(Y)))))&(![Y,Z,Pid0]: (((~setIn(Pid0,alive)|~elem(m_Down(Z),queue(host(Pid0))))|~host(Z)=host(Y))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(![Y,Z,Pid0]: (((((~setIn(Y,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Y))=elec_2)|~index(status,host(Pid0))=elec_2)|~elem(m_Ack(Y,Z),queue(host(Y))))))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|~leq(index(pendack,host(Y)),index(pendack,host(Z))))))&(![Y,Z,Pid0]: ((((leq(index(pendack,host(Pid0)),host(Y))|~setIn(Pid0,alive))|~elem(m_Halt(Pid0),queue(host(Z))))|~index(status,host(Pid0))=elec_2)|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(![Y,Z,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)=host(Z))|~host(Pid0)=nbr_proc)|~index(status,host(Pid0))=elec_1)|(~setIn(Y,alive)|~elem(m_Down(Z),queue(host(Y)))))))&(![Y,Z,Pid20,Pid0]: (((((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|~elem(m_Down(Pid20),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Z)=index(pendack,host(Pid0)))|~host(Pid20)=s(index(pendack,host(Pid0))))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&queue(host(X))=cons(m_NormQ(W),V))&(setIn(X,alive)&(~index(status,host(X))=norm&(?[Y,Z,X0,Y0]: (host(W)=host(Y0)&(host(X)=host(Y0)&(((((((setIn(Y0,alive)&elem(m_Down(X0),snoc(V,m_NotNorm(W))))&elem(m_Ack(Y0,Z),snoc(V,m_NotNorm(W))))&leq(nbr_proc,s(index(pendack,host(Y0)))))&index(status,host(Y0))=elec_2)&host(Z)=index(pendack,host(Y0)))&host(X0)=s(index(pendack,host(Y0))))&((setIn(Y,alive)&index(ldr,host(Y))=host(Y))&index(status,host(Y))=norm)))))))))),
% 98.39/12.85 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 98.39/12.85 fof(f213,plain,(
% 98.39/12.85 ?[V,W,X]: (((((((((((((((((![Y,Z]: (~elem(m_Ldr(Z),queue(host(Y)))|~leq(host(Y),host(Z))))&(![Y,Z]: (~elem(m_Down(Z),queue(host(Y)))|~host(Z)=host(Y))))&(![Y,Z]: (~elem(m_Halt(Z),queue(host(Y)))|~leq(host(Y),host(Z)))))&(![Y,Pid0]: ((![Z]: ~elem(m_Ack(Pid0,Y),queue(host(Z))))|~leq(host(Y),host(Pid0)))))&(![Y,Z]: ((Z=Y|~host(Z)=host(Y))|(~setIn(Y,alive)|~setIn(Z,alive)))))&(![Y,Z]: ((~setIn(Z,alive)|~elem(m_Ack(Z,Y),queue(host(Z))))|leq(host(Y),index(pendack,host(Z))))))&(![Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|(![Y]: ~elem(m_Ack(Z,Y),queue(host(Z)))))))&(![Y]: (((~index(status,host(Y))=elec_1&~index(status,host(Y))=elec_2)|~setIn(Y,alive))|index(elid,host(Y))=Y)))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|leq(index(pendack,host(Z)),host(Y)))))&(![Y]: ((![Z]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Down(Z),queue(host(Pid0)))))|~host(Z)=host(Y)))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(![Y,Z]: ((![Pid0]: ((((~setIn(Y,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Y))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Y,Z),queue(host(Y))))))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|~leq(index(pendack,host(Y)),index(pendack,host(Z))))))&(![Y]: ((![Pid0]: (((leq(index(pendack,host(Pid0)),host(Y))|~setIn(Pid0,alive))|(![Z]: ~elem(m_Halt(Pid0),queue(host(Z)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(![Z]: ((![Pid0]: ((((![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)=host(Z))|~host(Pid0)=nbr_proc)|~index(status,host(Pid0))=elec_1))|(![Y]: (~setIn(Y,alive)|~elem(m_Down(Z),queue(host(Y))))))))&((![Pid20,Pid0]: ((![Z]: (((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|~elem(m_Down(Pid20),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Z)=index(pendack,host(Pid0))))|~host(Pid20)=s(index(pendack,host(Pid0)))))|(![Y]: ((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&queue(host(X))=cons(m_NormQ(W),V))&(setIn(X,alive)&(~index(status,host(X))=norm&(?[Y0]: (host(W)=host(Y0)&(host(X)=host(Y0)&((?[X0]: ((?[Z]: (((((setIn(Y0,alive)&elem(m_Down(X0),snoc(V,m_NotNorm(W))))&elem(m_Ack(Y0,Z),snoc(V,m_NotNorm(W))))&leq(nbr_proc,s(index(pendack,host(Y0)))))&index(status,host(Y0))=elec_2)&host(Z)=index(pendack,host(Y0))))&host(X0)=s(index(pendack,host(Y0)))))&(?[Y]: ((setIn(Y,alive)&index(ldr,host(Y))=host(Y))&index(status,host(Y))=norm)))))))))),
% 98.39/12.85 inference(miniscoping,[status(thm)],[f212])).
% 98.39/12.85 fof(f214,plain,(
% 98.39/12.85 (((((((((((((((((![Y,Z]: (~elem(m_Ldr(Z),queue(host(Y)))|~leq(host(Y),host(Z))))&(![Y,Z]: (~elem(m_Down(Z),queue(host(Y)))|~host(Z)=host(Y))))&(![Y,Z]: (~elem(m_Halt(Z),queue(host(Y)))|~leq(host(Y),host(Z)))))&(![Y,Pid0]: ((![Z]: ~elem(m_Ack(Pid0,Y),queue(host(Z))))|~leq(host(Y),host(Pid0)))))&(![Y,Z]: ((Z=Y|~host(Z)=host(Y))|(~setIn(Y,alive)|~setIn(Z,alive)))))&(![Y,Z]: ((~setIn(Z,alive)|~elem(m_Ack(Z,Y),queue(host(Z))))|leq(host(Y),index(pendack,host(Z))))))&(![Z]: ((~setIn(Z,alive)|~index(status,host(Z))=elec_1)|(![Y]: ~elem(m_Ack(Z,Y),queue(host(Z)))))))&(![Y]: (((~index(status,host(Y))=elec_1&~index(status,host(Y))=elec_2)|~setIn(Y,alive))|index(elid,host(Y))=Y)))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|leq(index(pendack,host(Z)),host(Y)))))&(![Y]: ((![Z]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Down(Z),queue(host(Pid0)))))|~host(Z)=host(Y)))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(![Y,Z]: ((![Pid0]: ((((~setIn(Y,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Z))|~index(status,host(Y))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Y,Z),queue(host(Y))))))&(![Y,Z]: (((((leq(host(Y),host(Z))|~setIn(Y,alive))|~setIn(Z,alive))|~index(status,host(Y))=elec_2)|~index(status,host(Z))=elec_2)|~leq(index(pendack,host(Y)),index(pendack,host(Z))))))&(![Y]: ((![Pid0]: (((leq(index(pendack,host(Pid0)),host(Y))|~setIn(Pid0,alive))|(![Z]: ~elem(m_Halt(Pid0),queue(host(Z)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&(![Z]: ((![Pid0]: ((((![Pid20]: (((~leq(host(Pid0),sK7_skl(Pid20,Pid0,Z))&leq(s(zero),sK7_skl(Pid20,Pid0,Z)))&(~setIn(sK7_skl(Pid20,Pid0,Z),index(down,host(Pid0)))&~sK7_skl(Pid20,Pid0,Z)=host(Pid20)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid0)=host(Z))|~host(Pid0)=nbr_proc)|~index(status,host(Pid0))=elec_1))|(![Y]: (~setIn(Y,alive)|~elem(m_Down(Z),queue(host(Y))))))))&((![Pid20,Pid0]: ((![Z]: (((((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|~elem(m_Down(Pid20),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Z)=index(pendack,host(Pid0))))|~host(Pid20)=s(index(pendack,host(Pid0)))))|(![Y]: ((~setIn(Y,alive)|~index(ldr,host(Y))=host(Y))|~index(status,host(Y))=norm))))&queue(host(sK6_skl))=cons(m_NormQ(sK5_skl),sK4_skl))&(setIn(sK6_skl,alive)&(~index(status,host(sK6_skl))=norm&(host(sK5_skl)=host(sK8_skl)&(host(sK6_skl)=host(sK8_skl)&(((((((setIn(sK8_skl,alive)&elem(m_Down(sK9_skl),snoc(sK4_skl,m_NotNorm(sK5_skl))))&elem(m_Ack(sK8_skl,sK10_skl),snoc(sK4_skl,m_NotNorm(sK5_skl))))&leq(nbr_proc,s(index(pendack,host(sK8_skl)))))&index(status,host(sK8_skl))=elec_2)&host(sK10_skl)=index(pendack,host(sK8_skl)))&host(sK9_skl)=s(index(pendack,host(sK8_skl))))&((setIn(sK11_skl,alive)&index(ldr,host(sK11_skl))=host(sK11_skl))&index(status,host(sK11_skl))=norm)))))))),
% 98.39/12.85 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl]),skolemize(V,sK4_skl),skolemize(W,sK5_skl),skolemize(X,sK6_skl),skolemize(V0,sK7_skl(Pid20,Pid0,Z)),skolemize(Y0,sK8_skl),skolemize(X0,sK9_skl),skolemize(Z,sK10_skl),skolemize(Y,sK11_skl)],[f213])).
% 98.39/12.85 fof(f219,plain,(
% 98.39/12.85 ![X0,X1]: (X0=X1|~host(X0)=host(X1)|~setIn(X1,alive)|~setIn(X0,alive))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f233,plain,(
% 98.39/12.85 ![X0,X1,X2,X3]: (~setIn(X0,alive)|~elem(m_Ack(X0,X1),queue(host(X0)))|~elem(m_Down(X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X1)=index(pendack,host(X0))|~host(X2)=s(index(pendack,host(X0)))|~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f234,plain,(
% 98.39/12.85 queue(host(sK6_skl))=cons(m_NormQ(sK5_skl),sK4_skl)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f235,plain,(
% 98.39/12.85 setIn(sK6_skl,alive)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f237,plain,(
% 98.39/12.85 host(sK5_skl)=host(sK8_skl)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f238,plain,(
% 98.39/12.85 host(sK6_skl)=host(sK8_skl)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f239,plain,(
% 98.39/12.85 setIn(sK8_skl,alive)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f240,plain,(
% 98.39/12.85 elem(m_Down(sK9_skl),snoc(sK4_skl,m_NotNorm(sK5_skl)))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f241,plain,(
% 98.39/12.85 elem(m_Ack(sK8_skl,sK10_skl),snoc(sK4_skl,m_NotNorm(sK5_skl)))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f242,plain,(
% 98.39/12.85 leq(nbr_proc,s(index(pendack,host(sK8_skl))))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f243,plain,(
% 98.39/12.85 index(status,host(sK8_skl))=elec_2),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f244,plain,(
% 98.39/12.85 host(sK10_skl)=index(pendack,host(sK8_skl))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f245,plain,(
% 98.39/12.85 host(sK9_skl)=s(index(pendack,host(sK8_skl)))),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f246,plain,(
% 98.39/12.85 setIn(sK11_skl,alive)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f247,plain,(
% 98.39/12.85 index(ldr,host(sK11_skl))=host(sK11_skl)),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f248,plain,(
% 98.39/12.85 index(status,host(sK11_skl))=norm),
% 98.39/12.85 inference(cnf_transformation,[status(thm)],[f214])).
% 98.39/12.85 fof(f249,definition,(
% 98.39/12.85 ![X0,X1,X2]: (sQ0_spl <=> (~setIn(X0,alive)|~elem(m_Ack(X0,X1),queue(host(X0)))|~elem(m_Down(X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X1)=index(pendack,host(X0))|~host(X2)=s(index(pendack,host(X0)))))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f250,plain,(
% 98.39/12.85 ![X0,X1,X2]: (~setIn(X0,alive)|~elem(m_Ack(X0,X1),queue(host(X0)))|~elem(m_Down(X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X1)=index(pendack,host(X0))|~host(X2)=s(index(pendack,host(X0)))|~sQ0_spl)),
% 98.39/12.85 inference(component_clause,[status(thm)],[f249])).
% 98.39/12.85 fof(f252,definition,(
% 98.39/12.85 ![X3]: (sQ1_spl <=> (~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f253,plain,(
% 98.39/12.85 ![X0]: (~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ1_spl)),
% 98.39/12.85 inference(component_clause,[status(thm)],[f252])).
% 98.39/12.85 fof(f255,plain,(
% 98.39/12.85 sQ0_spl|sQ1_spl),
% 98.39/12.85 inference(split_clause,[status(thm)],[f233,f249,f252])).
% 98.39/12.85 fof(f282,plain,(
% 98.39/12.85 host(sK6_skl)=host(sK5_skl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f238])).
% 98.39/12.85 fof(f301,plain,(
% 98.39/12.85 index(status,host(sK5_skl))=elec_2),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f243])).
% 98.39/12.85 fof(f307,plain,(
% 98.39/12.85 ![X0]: (~leq(s(s(X0)),X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f210,f191])).
% 98.39/12.85 fof(f308,plain,(
% 98.39/12.85 ![X0]: (~leq(s(s(s(X0))),X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f307,f210])).
% 98.39/12.85 fof(f311,plain,(
% 98.39/12.85 ![X0]: (~leq(s(s(s(s(X0)))),X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f308,f210])).
% 98.39/12.85 fof(f317,plain,(
% 98.39/12.85 host(sK10_skl)=index(pendack,host(sK5_skl))),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f244])).
% 98.39/12.85 fof(f321,plain,(
% 98.39/12.85 ![X0,X1]: (leq(X0,X1)|~leq(s(X0),X1))),
% 98.39/12.85 inference(resolution,[status(thm)],[f205,f210])).
% 98.39/12.85 fof(f326,plain,(
% 98.39/12.85 ![X0,X1]: (leq(X0,s(X1))|~leq(s(X0),X1))),
% 98.39/12.85 inference(resolution,[status(thm)],[f321,f210])).
% 98.39/12.85 fof(f337,plain,(
% 98.39/12.85 ![X0]: (~leq(s(s(s(s(s(X0))))),X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f311,f210])).
% 98.39/12.85 fof(f340,plain,(
% 98.39/12.85 ![X0,X1]: (leq(X0,s(s(X1)))|~leq(X0,X1))),
% 98.39/12.85 inference(resolution,[status(thm)],[f326,f204])).
% 98.39/12.85 fof(f348,plain,(
% 98.39/12.85 ![X0]: (X0=sK8_skl|~host(X0)=host(sK8_skl)|~setIn(X0,alive))),
% 98.39/12.85 inference(resolution,[status(thm)],[f219,f239])).
% 98.39/12.85 fof(f350,plain,(
% 98.39/12.85 ![X0]: (X0=sK8_skl|~host(X0)=host(sK5_skl)|~setIn(X0,alive))),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f348])).
% 98.39/12.85 fof(f354,plain,(
% 98.39/12.85 ![X0]: (~leq(s(s(s(s(s(s(X0)))))),X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f340,f311])).
% 98.39/12.85 fof(f400,plain,(
% 98.39/12.85 queue(host(sK5_skl))=cons(m_NormQ(sK5_skl),sK4_skl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f282,f234])).
% 98.39/12.85 fof(f416,plain,(
% 98.39/12.85 host(sK9_skl)=s(index(pendack,host(sK5_skl)))),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f245])).
% 98.39/12.85 fof(f417,plain,(
% 98.39/12.85 host(sK9_skl)=s(host(sK10_skl))),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f317,f416])).
% 98.39/12.85 fof(f429,plain,(
% 98.39/12.85 ![X0]: (leq(host(sK10_skl),X0)|~leq(host(sK9_skl),s(X0)))),
% 98.39/12.85 inference(paramodulation,[status(thm)],[f417,f205])).
% 98.39/12.85 fof(f434,plain,(
% 98.39/12.85 ![X0]: (leq(X0,host(sK9_skl))|~leq(X0,host(sK10_skl)))),
% 98.39/12.85 inference(paramodulation,[status(thm)],[f417,f210])).
% 98.39/12.85 fof(f435,plain,(
% 98.39/12.85 ~leq(host(sK9_skl),host(sK10_skl))),
% 98.39/12.85 inference(paramodulation,[status(thm)],[f417,f191])).
% 98.39/12.85 fof(f447,definition,(
% 98.39/12.85 sQ12_spl <=> (setIn(sK8_skl,alive))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f449,plain,(
% 98.39/12.85 ~setIn(sK8_skl,alive)|sQ12_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f447])).
% 98.39/12.85 fof(f454,plain,(
% 98.39/12.85 $false|sQ12_spl),
% 98.39/12.85 inference(forward_subsumption_resolution,[status(thm)],[f449,f239])).
% 98.39/12.85 fof(f455,plain,(
% 98.39/12.85 sQ12_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f454])).
% 98.39/12.85 fof(f471,plain,(
% 98.39/12.85 ![X0]: (elem(X0,queue(host(sK5_skl)))|~elem(X0,sK4_skl))),
% 98.39/12.85 inference(paramodulation,[status(thm)],[f400,f142])).
% 98.39/12.85 fof(f472,plain,(
% 98.39/12.85 m_Down(sK9_skl)=m_NotNorm(sK5_skl)|elem(m_Down(sK9_skl),sK4_skl)),
% 98.39/12.85 inference(resolution,[status(thm)],[f145,f240])).
% 98.39/12.85 fof(f474,definition,(
% 98.39/12.85 sQ16_spl <=> (m_Down(sK9_skl)=m_NotNorm(sK5_skl))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f475,plain,(
% 98.39/12.85 m_Down(sK9_skl)=m_NotNorm(sK5_skl)|~sQ16_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f474])).
% 98.39/12.85 fof(f477,definition,(
% 98.39/12.85 sQ17_spl <=> (elem(m_Down(sK9_skl),sK4_skl))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f478,plain,(
% 98.39/12.85 elem(m_Down(sK9_skl),sK4_skl)|~sQ17_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f477])).
% 98.39/12.85 fof(f480,plain,(
% 98.39/12.85 sQ16_spl|sQ17_spl),
% 98.39/12.85 inference(split_clause,[status(thm)],[f472,f474,f477])).
% 98.39/12.85 fof(f481,plain,(
% 98.39/12.85 $false|~sQ16_spl),
% 98.39/12.85 inference(forward_subsumption_resolution,[status(thm)],[f475,f91])).
% 98.39/12.85 fof(f482,plain,(
% 98.39/12.85 ~sQ16_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f481])).
% 98.39/12.85 fof(f484,plain,(
% 98.39/12.85 ![X0]: (~leq(s(s(s(s(s(s(s(X0))))))),X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f337,f340])).
% 98.39/12.85 fof(f737,definition,(
% 98.39/12.85 sQ35_spl <=> (leq(s(zero),host(sK9_skl)))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f739,plain,(
% 98.39/12.85 ~leq(s(zero),host(sK9_skl))|sQ35_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f737])).
% 98.39/12.85 fof(f768,definition,(
% 98.39/12.85 sQ36_spl <=> (s(zero)=s(s(s(s(nbr_proc)))))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f769,plain,(
% 98.39/12.85 s(zero)=s(s(s(s(nbr_proc))))|~sQ36_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f768])).
% 98.39/12.85 fof(f772,definition,(
% 98.39/12.85 sQ37_spl <=> (s(zero)=s(s(s(nbr_proc))))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f773,plain,(
% 98.39/12.85 s(zero)=s(s(s(nbr_proc)))|~sQ37_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f772])).
% 98.39/12.85 fof(f869,definition,(
% 98.39/12.85 sQ50_spl <=> (index(status,host(sK8_skl))=elec_2)),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f871,plain,(
% 98.39/12.85 ~index(status,host(sK8_skl))=elec_2|sQ50_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f869])).
% 98.39/12.85 fof(f1038,plain,(
% 98.39/12.85 ![X0,X1]: (leq(X0,s(X1))|leq(X1,X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f193,f321])).
% 98.39/12.85 fof(f1049,plain,(
% 98.39/12.85 ![X0]: (leq(host(sK10_skl),X0)|leq(X0,host(sK9_skl)))),
% 98.39/12.85 inference(resolution,[status(thm)],[f193,f434])).
% 98.39/12.85 fof(f1089,plain,(
% 98.39/12.85 ![X0]: (~leq(nbr_proc,host(X0))|nbr_proc=host(X0))),
% 98.39/12.85 inference(resolution,[status(thm)],[f196,f76])).
% 98.39/12.85 fof(f1382,plain,(
% 98.39/12.85 ![X0,X1,X2]: (~leq(s(X0),X1)|~leq(X1,X2)|leq(X0,s(X2)))),
% 98.39/12.85 inference(resolution,[status(thm)],[f201,f326])).
% 98.39/12.85 fof(f1578,definition,(
% 98.39/12.85 sQ79_spl <=> (leq(host(sK10_skl),nbr_proc))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f1646,definition,(
% 98.39/12.85 sQ83_spl <=> (nbr_proc=host(sK10_skl))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f1647,plain,(
% 98.39/12.85 nbr_proc=host(sK10_skl)|~sQ83_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f1646])).
% 98.39/12.85 fof(f1953,definition,(
% 98.39/12.85 sQ90_spl <=> (m_Ack(sK6_skl,sK10_skl)=m_NotNorm(sK5_skl))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f1954,plain,(
% 98.39/12.85 m_Ack(sK6_skl,sK10_skl)=m_NotNorm(sK5_skl)|~sQ90_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f1953])).
% 98.39/12.85 fof(f1956,definition,(
% 98.39/12.85 sQ91_spl <=> (elem(m_Ack(sK6_skl,sK10_skl),sK4_skl))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f1957,plain,(
% 98.39/12.85 elem(m_Ack(sK6_skl,sK10_skl),sK4_skl)|~sQ91_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f1956])).
% 98.39/12.85 fof(f2097,plain,(
% 98.39/12.85 leq(nbr_proc,s(index(pendack,host(sK5_skl))))),
% 98.39/12.85 inference(backward_demodulation,[status(thm)],[f237,f242])).
% 98.39/12.85 fof(f2198,plain,(
% 98.39/12.85 ![X0,X1]: (~setIn(sK8_skl,alive)|~elem(m_Ack(sK8_skl,X0),queue(host(sK8_skl)))|~elem(m_Down(X1),queue(host(sK5_skl)))|~leq(nbr_proc,s(index(pendack,host(sK8_skl))))|~index(status,host(sK8_skl))=elec_2|~host(X0)=index(pendack,host(sK8_skl))|~host(X1)=s(index(pendack,host(sK8_skl)))|~sQ0_spl)),
% 98.39/12.85 inference(paramodulation,[status(thm)],[f237,f250])).
% 98.39/12.85 fof(f2200,definition,(
% 98.39/12.85 ![X0]: (sQ113_spl <=> (~elem(m_Ack(sK8_skl,X0),queue(host(sK8_skl)))|~host(X0)=index(pendack,host(sK8_skl))))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f2201,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Ack(sK8_skl,X0),queue(host(sK8_skl)))|~host(X0)=index(pendack,host(sK8_skl))|~sQ113_spl)),
% 98.39/12.85 inference(component_clause,[status(thm)],[f2200])).
% 98.39/12.85 fof(f2203,definition,(
% 98.39/12.85 ![X1]: (sQ114_spl <=> (~elem(m_Down(X1),queue(host(sK5_skl)))|~host(X1)=s(index(pendack,host(sK8_skl)))))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f2204,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Down(X0),queue(host(sK5_skl)))|~host(X0)=s(index(pendack,host(sK8_skl)))|~sQ114_spl)),
% 98.39/12.85 inference(component_clause,[status(thm)],[f2203])).
% 98.39/12.85 fof(f2206,definition,(
% 98.39/12.85 sQ115_spl <=> (leq(nbr_proc,s(index(pendack,host(sK8_skl)))))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f2208,plain,(
% 98.39/12.85 ~leq(nbr_proc,s(index(pendack,host(sK8_skl))))|sQ115_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f2206])).
% 98.39/12.85 fof(f2209,plain,(
% 98.39/12.85 ~sQ12_spl|sQ113_spl|sQ114_spl|~sQ115_spl|~sQ50_spl|~sQ0_spl),
% 98.39/12.85 inference(split_clause,[status(thm)],[f2198,f447,f2200,f2203,f2206,f869,f249])).
% 98.39/12.85 fof(f2224,plain,(
% 98.39/12.85 ~leq(nbr_proc,s(index(pendack,host(sK5_skl))))|sQ115_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f2208])).
% 98.39/12.85 fof(f2225,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Down(X0),queue(host(sK5_skl)))|~host(X0)=s(index(pendack,host(sK5_skl)))|~sQ114_spl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f2204])).
% 98.39/12.85 fof(f2226,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Ack(sK8_skl,X0),queue(host(sK5_skl)))|~host(X0)=index(pendack,host(sK8_skl))|~sQ113_spl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f2201])).
% 98.39/12.85 fof(f2227,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Ack(sK8_skl,X0),queue(host(sK5_skl)))|~host(X0)=index(pendack,host(sK5_skl))|~sQ113_spl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f237,f2226])).
% 98.39/12.85 fof(f2347,plain,(
% 98.39/12.85 leq(nbr_proc,s(host(sK10_skl)))),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f317,f2097])).
% 98.39/12.85 fof(f2348,plain,(
% 98.39/12.85 leq(nbr_proc,host(sK9_skl))),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f417,f2347])).
% 98.39/12.85 fof(f2351,plain,(
% 98.39/12.85 nbr_proc=host(sK9_skl)),
% 98.39/12.85 inference(resolution,[status(thm)],[f2348,f1089])).
% 98.39/12.85 fof(f2369,plain,(
% 98.39/12.85 ~leq(s(zero),nbr_proc)|~sQ37_spl),
% 98.39/12.85 inference(paramodulation,[status(thm)],[f773,f308])).
% 98.39/12.85 fof(f2506,plain,(
% 98.39/12.85 sK6_skl=sK8_skl|~host(sK6_skl)=host(sK5_skl)),
% 98.39/12.85 inference(resolution,[status(thm)],[f350,f235])).
% 98.39/12.85 fof(f2518,definition,(
% 98.39/12.85 sQ136_spl <=> (sK6_skl=sK8_skl)),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f2519,plain,(
% 98.39/12.85 sK6_skl=sK8_skl|~sQ136_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f2518])).
% 98.39/12.85 fof(f2521,definition,(
% 98.39/12.85 sQ137_spl <=> (host(sK6_skl)=host(sK5_skl))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f2523,plain,(
% 98.39/12.85 ~host(sK6_skl)=host(sK5_skl)|sQ137_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f2521])).
% 98.39/12.85 fof(f2524,plain,(
% 98.39/12.85 sQ136_spl|~sQ137_spl),
% 98.39/12.85 inference(split_clause,[status(thm)],[f2506,f2518,f2521])).
% 98.39/12.85 fof(f2525,plain,(
% 98.39/12.85 ~host(sK5_skl)=host(sK5_skl)|sQ137_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f282,f2523])).
% 98.39/12.85 fof(f2526,plain,(
% 98.39/12.85 $false|sQ137_spl),
% 98.39/12.85 inference(trivial_equality_resolution,[status(thm)],[f2525])).
% 98.39/12.85 fof(f2527,plain,(
% 98.39/12.85 sQ137_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f2526])).
% 98.39/12.85 fof(f2552,plain,(
% 98.39/12.85 elem(m_Ack(sK6_skl,sK10_skl),snoc(sK4_skl,m_NotNorm(sK5_skl)))|~sQ136_spl),
% 98.39/12.85 inference(backward_demodulation,[status(thm)],[f2519,f241])).
% 98.39/12.85 fof(f2566,plain,(
% 98.39/12.85 m_Ack(sK6_skl,sK10_skl)=m_NotNorm(sK5_skl)|elem(m_Ack(sK6_skl,sK10_skl),sK4_skl)|~sQ136_spl),
% 98.39/12.85 inference(resolution,[status(thm)],[f2552,f145])).
% 98.39/12.85 fof(f2567,plain,(
% 98.39/12.85 sQ90_spl|sQ91_spl|~sQ136_spl),
% 98.39/12.85 inference(split_clause,[status(thm)],[f2566,f1953,f1956,f2518])).
% 98.39/12.85 fof(f2568,plain,(
% 98.39/12.85 $false|~sQ90_spl),
% 98.39/12.85 inference(forward_subsumption_resolution,[status(thm)],[f1954,f85])).
% 98.39/12.85 fof(f2569,plain,(
% 98.39/12.85 ~sQ90_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f2568])).
% 98.39/12.85 fof(f2965,plain,(
% 98.39/12.85 elem(m_Down(sK9_skl),queue(host(sK5_skl)))|~sQ17_spl),
% 98.39/12.85 inference(resolution,[status(thm)],[f471,f478])).
% 98.39/12.85 fof(f3002,definition,(
% 98.39/12.85 sQ158_spl <=> (leq(nbr_proc,s(index(pendack,host(sK5_skl)))))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f3004,plain,(
% 98.39/12.85 ~leq(nbr_proc,s(index(pendack,host(sK5_skl))))|sQ158_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f3002])).
% 98.39/12.85 fof(f3039,plain,(
% 98.39/12.85 ~leq(nbr_proc,s(host(sK10_skl)))|sQ158_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f317,f3004])).
% 98.39/12.85 fof(f3040,plain,(
% 98.39/12.85 ~leq(nbr_proc,host(sK9_skl))|sQ158_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f417,f3039])).
% 98.39/12.85 fof(f3041,plain,(
% 98.39/12.85 $false|sQ158_spl),
% 98.39/12.85 inference(forward_subsumption_resolution,[status(thm)],[f3040,f2348])).
% 98.39/12.85 fof(f3042,plain,(
% 98.39/12.85 sQ158_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f3041])).
% 98.39/12.85 fof(f3088,plain,(
% 98.39/12.85 ~leq(s(zero),nbr_proc)|~sQ36_spl),
% 98.39/12.85 inference(paramodulation,[status(thm)],[f769,f311])).
% 98.39/12.85 fof(f5432,plain,(
% 98.39/12.85 ~index(status,host(sK6_skl))=elec_2|~sQ136_spl|sQ50_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f2519,f871])).
% 98.39/12.85 fof(f5433,plain,(
% 98.39/12.85 ~index(status,host(sK5_skl))=elec_2|~sQ136_spl|sQ50_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f282,f5432])).
% 98.39/12.85 fof(f5434,plain,(
% 98.39/12.85 ~elec_2=elec_2|~sQ136_spl|sQ50_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f301,f5433])).
% 98.39/12.85 fof(f5435,plain,(
% 98.39/12.85 $false|~sQ136_spl|sQ50_spl),
% 98.39/12.85 inference(trivial_equality_resolution,[status(thm)],[f5434])).
% 98.39/12.85 fof(f5436,plain,(
% 98.39/12.85 ~sQ136_spl|sQ50_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f5435])).
% 98.39/12.85 fof(f5450,plain,(
% 98.39/12.85 ~sQ158_spl|sQ115_spl),
% 98.39/12.85 inference(split_clause,[status(thm)],[f2224,f3002,f2206])).
% 98.39/12.85 fof(f5453,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Ack(sK6_skl,X0),queue(host(sK5_skl)))|~host(X0)=index(pendack,host(sK5_skl))|~sQ136_spl|~sQ113_spl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f2519,f2227])).
% 98.39/12.85 fof(f5454,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Ack(sK6_skl,X0),queue(host(sK5_skl)))|~host(X0)=host(sK10_skl)|~sQ136_spl|~sQ113_spl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f317,f5453])).
% 98.39/12.85 fof(f5736,plain,(
% 98.39/12.85 elem(m_Ack(sK6_skl,sK10_skl),queue(host(sK5_skl)))|~sQ91_spl),
% 98.39/12.85 inference(resolution,[status(thm)],[f1957,f471])).
% 98.39/12.85 fof(f6630,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Down(X0),queue(host(sK5_skl)))|~host(X0)=s(host(sK10_skl))|~sQ114_spl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f317,f2225])).
% 98.39/12.85 fof(f6631,plain,(
% 98.39/12.85 ![X0]: (~elem(m_Down(X0),queue(host(sK5_skl)))|~host(X0)=host(sK9_skl)|~sQ114_spl)),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f417,f6630])).
% 98.39/12.85 fof(f6762,plain,(
% 98.39/12.85 ~index(ldr,host(sK11_skl))=host(sK11_skl)|~index(status,host(sK11_skl))=norm|~sQ1_spl),
% 98.39/12.85 inference(resolution,[status(thm)],[f253,f246])).
% 98.39/12.85 fof(f6764,definition,(
% 98.39/12.85 sQ257_spl <=> (index(ldr,host(sK11_skl))=host(sK11_skl))),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f6766,plain,(
% 98.39/12.85 ~index(ldr,host(sK11_skl))=host(sK11_skl)|sQ257_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f6764])).
% 98.39/12.85 fof(f6767,definition,(
% 98.39/12.85 sQ258_spl <=> (index(status,host(sK11_skl))=norm)),
% 98.39/12.85 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 98.39/12.85 fof(f6769,plain,(
% 98.39/12.85 ~index(status,host(sK11_skl))=norm|sQ258_spl),
% 98.39/12.85 inference(component_clause,[status(thm)],[f6767])).
% 98.39/12.85 fof(f6770,plain,(
% 98.39/12.85 ~sQ257_spl|~sQ258_spl|~sQ1_spl),
% 98.39/12.85 inference(split_clause,[status(thm)],[f6762,f6764,f6767,f252])).
% 98.39/12.85 fof(f8163,plain,(
% 98.39/12.85 ~norm=norm|sQ258_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f248,f6769])).
% 98.39/12.85 fof(f8164,plain,(
% 98.39/12.85 $false|sQ258_spl),
% 98.39/12.85 inference(trivial_equality_resolution,[status(thm)],[f8163])).
% 98.39/12.85 fof(f8165,plain,(
% 98.39/12.85 sQ258_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f8164])).
% 98.39/12.85 fof(f8204,plain,(
% 98.39/12.85 ~host(sK11_skl)=host(sK11_skl)|sQ257_spl),
% 98.39/12.85 inference(forward_demodulation,[status(thm)],[f247,f6766])).
% 98.39/12.85 fof(f8205,plain,(
% 98.39/12.85 $false|sQ257_spl),
% 98.39/12.85 inference(trivial_equality_resolution,[status(thm)],[f8204])).
% 98.39/12.85 fof(f8206,plain,(
% 98.39/12.85 sQ257_spl),
% 98.39/12.85 inference(contradiction_clause,[status(thm)],[f8205])).
% 98.39/12.86 fof(f8297,definition,(
% 98.39/12.86 ![X0]: (sQ292_spl <=> (q_nil=cons(X0,init(q_nil))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f8298,plain,(
% 98.39/12.86 ![X0]: (q_nil=cons(X0,init(q_nil))|~sQ292_spl)),
% 98.39/12.86 inference(component_clause,[status(thm)],[f8297])).
% 98.39/12.86 fof(f8314,plain,(
% 98.39/12.86 $false|~sQ292_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f8298,f133])).
% 98.39/12.86 fof(f8315,plain,(
% 98.39/12.86 ~sQ292_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f8314])).
% 98.39/12.86 fof(f8322,plain,(
% 98.39/12.86 ![X0,X1]: (~leq(host(X0),X1)|leq(zero,s(X1)))),
% 98.39/12.86 inference(resolution,[status(thm)],[f1382,f74])).
% 98.39/12.86 fof(f8418,plain,(
% 98.39/12.86 ![X0,X1]: (leq(zero,s(X0))|leq(X0,host(X1)))),
% 98.39/12.86 inference(resolution,[status(thm)],[f8322,f193])).
% 98.39/12.86 fof(f8428,definition,(
% 98.39/12.86 ![X0]: (sQ295_spl <=> (leq(zero,s(host(X0)))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ295_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f8511,plain,(
% 98.39/12.86 ![X0,X1]: (leq(zero,s(host(X0)))|leq(zero,s(host(X1))))),
% 98.39/12.86 inference(resolution,[status(thm)],[f8418,f8322])).
% 98.39/12.86 fof(f8534,plain,(
% 98.39/12.86 sQ295_spl),
% 98.39/12.86 inference(split_clause,[status(thm)],[f8511,f8428])).
% 98.39/12.86 fof(f10557,definition,(
% 98.39/12.86 ![X0]: (sQ318_spl <=> (~leq(host(X0),nbr_proc)))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f10558,plain,(
% 98.39/12.86 ![X0]: (~leq(host(X0),nbr_proc)|~sQ318_spl)),
% 98.39/12.86 inference(component_clause,[status(thm)],[f10557])).
% 98.39/12.86 fof(f10580,plain,(
% 98.39/12.86 $false|~sQ318_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f10558,f76])).
% 98.39/12.86 fof(f10581,plain,(
% 98.39/12.86 ~sQ318_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f10580])).
% 98.39/12.86 fof(f10704,definition,(
% 98.39/12.86 ![X0]: (sQ320_spl <=> (~leq(host(sK9_skl),host(X0))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f10705,plain,(
% 98.39/12.86 ![X0]: (~leq(host(sK9_skl),host(X0))|~sQ320_spl)),
% 98.39/12.86 inference(component_clause,[status(thm)],[f10704])).
% 98.39/12.86 fof(f10712,definition,(
% 98.39/12.86 ![X0,X1]: (sQ322_spl <=> (~leq(host(X0),host(X1))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f10713,plain,(
% 98.39/12.86 ![X0,X1]: (~leq(host(X0),host(X1))|~sQ322_spl)),
% 98.39/12.86 inference(component_clause,[status(thm)],[f10712])).
% 98.39/12.86 fof(f10718,definition,(
% 98.39/12.86 ![X0,X1]: (sQ323_spl <=> (leq(host(X0),host(X1))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f10719,plain,(
% 98.39/12.86 ![X0,X1]: (leq(host(X0),host(X1))|~sQ323_spl)),
% 98.39/12.86 inference(component_clause,[status(thm)],[f10718])).
% 98.39/12.86 fof(f10743,plain,(
% 98.39/12.86 $false|~sQ323_spl),
% 98.39/12.86 inference(backward_subsumption_resolution,[status(thm)],[f435,f10719])).
% 98.39/12.86 fof(f10759,plain,(
% 98.39/12.86 ~sQ323_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f10743])).
% 98.39/12.86 fof(f10760,plain,(
% 98.39/12.86 ![X0]: (leq(host(X0),host(sK9_skl))|~sQ322_spl)),
% 98.39/12.86 inference(resolution,[status(thm)],[f10713,f1049])).
% 98.39/12.86 fof(f10774,plain,(
% 98.39/12.86 $false|~sQ322_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f10760,f10713])).
% 98.39/12.86 fof(f10775,plain,(
% 98.39/12.86 ~sQ322_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f10774])).
% 98.39/12.86 fof(f10814,plain,(
% 98.39/12.86 $false|~sQ320_spl),
% 98.39/12.86 inference(resolution,[status(thm)],[f10705,f193])).
% 98.39/12.86 fof(f10821,plain,(
% 98.39/12.86 ~sQ320_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f10814])).
% 98.39/12.86 fof(f11618,definition,(
% 98.39/12.86 sQ331_spl <=> (leq(s(host(sK9_skl)),host(sK9_skl)))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f11619,plain,(
% 98.39/12.86 leq(s(host(sK9_skl)),host(sK9_skl))|~sQ331_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f11618])).
% 98.39/12.86 fof(f11637,plain,(
% 98.39/12.86 $false|~sQ331_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f11619,f191])).
% 98.39/12.86 fof(f11638,plain,(
% 98.39/12.86 ~sQ331_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f11637])).
% 98.39/12.86 fof(f11874,plain,(
% 98.39/12.86 ![X0]: (~leq(X0,host(sK10_skl))|leq(s(X0),host(sK9_skl)))),
% 98.39/12.86 inference(paramodulation,[status(thm)],[f417,f204])).
% 98.39/12.86 fof(f11878,plain,(
% 98.39/12.86 ![X0]: (leq(X0,host(sK9_skl))|~leq(X0,host(sK10_skl)))),
% 98.39/12.86 inference(paramodulation,[status(thm)],[f417,f210])).
% 98.39/12.86 fof(f11964,definition,(
% 98.39/12.86 sQ353_spl <=> (leq(host(sK5_skl),nbr_proc))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f11966,plain,(
% 98.39/12.86 ~leq(host(sK5_skl),nbr_proc)|sQ353_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f11964])).
% 98.39/12.86 fof(f11972,plain,(
% 98.39/12.86 $false|sQ353_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f11966,f76])).
% 98.39/12.86 fof(f11973,plain,(
% 98.39/12.86 sQ353_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f11972])).
% 98.39/12.86 fof(f12279,plain,(
% 98.39/12.86 ~host(sK10_skl)=host(sK9_skl)),
% 98.39/12.86 inference(resolution,[status(thm)],[f417,f73])).
% 98.39/12.86 fof(f12341,plain,(
% 98.39/12.86 ~leq(host(sK9_skl),host(sK10_skl))),
% 98.39/12.86 inference(paramodulation,[status(thm)],[f417,f191])).
% 98.39/12.86 fof(f12658,plain,(
% 98.39/12.86 ![X0]: (leq(host(sK10_skl),X0)|leq(X0,host(sK9_skl)))),
% 98.39/12.86 inference(resolution,[status(thm)],[f429,f1038])).
% 98.39/12.86 fof(f12833,definition,(
% 98.39/12.86 ![X0]: (sQ369_spl <=> (~leq(host(X0),host(sK5_skl))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f12834,plain,(
% 98.39/12.86 ![X0]: (~leq(host(X0),host(sK5_skl))|~sQ369_spl)),
% 98.39/12.86 inference(component_clause,[status(thm)],[f12833])).
% 98.39/12.86 fof(f12860,definition,(
% 98.39/12.86 sQ371_spl <=> (leq(host(sK5_skl),host(sK5_skl)))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f12862,plain,(
% 98.39/12.86 ~leq(host(sK5_skl),host(sK5_skl))|sQ371_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f12860])).
% 98.39/12.86 fof(f12869,plain,(
% 98.39/12.86 $false|sQ371_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f12862,f192])).
% 98.39/12.86 fof(f12870,plain,(
% 98.39/12.86 sQ371_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f12869])).
% 98.39/12.86 fof(f12878,plain,(
% 98.39/12.86 $false|~sQ369_spl),
% 98.39/12.86 inference(resolution,[status(thm)],[f12834,f193])).
% 98.39/12.86 fof(f12887,plain,(
% 98.39/12.86 ~sQ369_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f12878])).
% 98.39/12.86 fof(f13821,definition,(
% 98.39/12.86 sQ392_spl <=> (leq(s(nbr_proc),s(nbr_proc)))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f13823,plain,(
% 98.39/12.86 ~leq(s(nbr_proc),s(nbr_proc))|sQ392_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f13821])).
% 98.39/12.86 fof(f13840,plain,(
% 98.39/12.86 $false|sQ392_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f13823,f192])).
% 98.39/12.86 fof(f13841,plain,(
% 98.39/12.86 sQ392_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f13840])).
% 98.39/12.86 fof(f13915,definition,(
% 98.39/12.86 sQ403_spl <=> (leq(host(sK9_skl),s(host(sK10_skl))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f13917,plain,(
% 98.39/12.86 ~leq(host(sK9_skl),s(host(sK10_skl)))|sQ403_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f13915])).
% 98.39/12.86 fof(f13918,definition,(
% 98.39/12.86 sQ404_spl <=> (leq(s(host(sK10_skl)),host(sK10_skl)))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f13919,plain,(
% 98.39/12.86 leq(s(host(sK10_skl)),host(sK10_skl))|~sQ404_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f13918])).
% 98.39/12.86 fof(f13939,plain,(
% 98.39/12.86 leq(host(sK9_skl),host(sK10_skl))|~sQ404_spl),
% 98.39/12.86 inference(forward_demodulation,[status(thm)],[f417,f13919])).
% 98.39/12.86 fof(f13940,plain,(
% 98.39/12.86 $false|~sQ404_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f13939,f12341])).
% 98.39/12.86 fof(f13941,plain,(
% 98.39/12.86 ~sQ404_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f13940])).
% 98.39/12.86 fof(f14165,plain,(
% 98.39/12.86 $false|sQ35_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f739,f74])).
% 98.39/12.86 fof(f14166,plain,(
% 98.39/12.86 sQ35_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f14165])).
% 98.39/12.86 fof(f14578,definition,(
% 98.39/12.86 sQ411_spl <=> (leq(s(nbr_proc),nbr_proc))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f14579,plain,(
% 98.39/12.86 leq(s(nbr_proc),nbr_proc)|~sQ411_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f14578])).
% 98.39/12.86 fof(f14600,plain,(
% 98.39/12.86 $false|~sQ411_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f14579,f191])).
% 98.39/12.86 fof(f14601,plain,(
% 98.39/12.86 ~sQ411_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f14600])).
% 98.39/12.86 fof(f14760,definition,(
% 98.39/12.86 sQ416_spl <=> (leq(s(host(sK5_skl)),host(sK5_skl)))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f14761,plain,(
% 98.39/12.86 leq(s(host(sK5_skl)),host(sK5_skl))|~sQ416_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f14760])).
% 98.39/12.86 fof(f14767,plain,(
% 98.39/12.86 $false|~sQ416_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f14761,f191])).
% 98.39/12.86 fof(f14768,plain,(
% 98.39/12.86 ~sQ416_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f14767])).
% 98.39/12.86 fof(f14876,definition,(
% 98.39/12.86 sQ418_spl <=> (s(host(sK10_skl))=s(s(s(nbr_proc))))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f14877,plain,(
% 98.39/12.86 s(host(sK10_skl))=s(s(s(nbr_proc)))|~sQ418_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f14876])).
% 98.39/12.86 fof(f15335,definition,(
% 98.39/12.86 sQ430_spl <=> (leq(s(s(nbr_proc)),nbr_proc))),
% 98.39/12.86 introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition])).
% 98.39/12.86 fof(f15336,plain,(
% 98.39/12.86 leq(s(s(nbr_proc)),nbr_proc)|~sQ430_spl),
% 98.39/12.86 inference(component_clause,[status(thm)],[f15335])).
% 98.39/12.86 fof(f15357,plain,(
% 98.39/12.86 $false|~sQ430_spl),
% 98.39/12.86 inference(forward_subsumption_resolution,[status(thm)],[f15336,f307])).
% 98.39/12.86 fof(f15358,plain,(
% 98.39/12.86 ~sQ430_spl),
% 98.39/12.86 inference(contradiction_clause,[status(thm)],[f15357])).
% 98.39/12.87 fof(f15549,definition,(
% 98.39/12.87 sQ435_spl <=> (leq(index(pendack,host(sK11_skl)),index(pendack,host(sK11_skl))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f15551,plain,(
% 98.39/12.87 ~leq(index(pendack,host(sK11_skl)),index(pendack,host(sK11_skl)))|sQ435_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f15549])).
% 98.39/12.87 fof(f15563,plain,(
% 98.39/12.87 $false|sQ435_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f15551,f192])).
% 98.39/12.87 fof(f15564,plain,(
% 98.39/12.87 sQ435_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f15563])).
% 98.39/12.87 fof(f16735,definition,(
% 98.39/12.87 sQ472_spl <=> (s(s(zero))=s(s(nbr_proc)))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f16736,plain,(
% 98.39/12.87 s(s(zero))=s(s(nbr_proc))|~sQ472_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f16735])).
% 98.39/12.87 fof(f17039,definition,(
% 98.39/12.87 sQ479_spl <=> (host(sK11_skl)=s(nbr_proc))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ479_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f17040,plain,(
% 98.39/12.87 host(sK11_skl)=s(nbr_proc)|~sQ479_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f17039])).
% 98.39/12.87 fof(f17124,plain,(
% 98.39/12.87 ~leq(host(sK11_skl),nbr_proc)|~sQ479_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f17040,f191])).
% 98.39/12.87 fof(f17153,plain,(
% 98.39/12.87 $false|~sQ479_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f17124,f76])).
% 98.39/12.87 fof(f17154,plain,(
% 98.39/12.87 ~sQ479_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f17153])).
% 98.39/12.87 fof(f17945,definition,(
% 98.39/12.87 ![X0]: (sQ508_spl <=> (nbr_proc=host(X0)|~leq(host(sK10_skl),host(X0))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ508_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f17946,plain,(
% 98.39/12.87 ![X0]: (nbr_proc=host(X0)|~leq(host(sK10_skl),host(X0))|~sQ508_spl)),
% 98.39/12.87 inference(component_clause,[status(thm)],[f17945])).
% 98.39/12.87 fof(f18527,definition,(
% 98.39/12.87 sQ514_spl <=> (s(s(nbr_proc))=s(host(sK9_skl)))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f18528,plain,(
% 98.39/12.87 s(s(nbr_proc))=s(host(sK9_skl))|~sQ514_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f18527])).
% 98.39/12.87 fof(f19296,plain,(
% 98.39/12.87 ~host(sK10_skl)=nbr_proc),
% 98.39/12.87 inference(backward_demodulation,[status(thm)],[f2351,f12279])).
% 98.39/12.87 fof(f19297,plain,(
% 98.39/12.87 ![X0]: (leq(X0,nbr_proc)|~leq(X0,host(sK10_skl)))),
% 98.39/12.87 inference(backward_demodulation,[status(thm)],[f2351,f11878])).
% 98.39/12.87 fof(f19299,plain,(
% 98.39/12.87 ![X0]: (~leq(X0,host(sK10_skl))|leq(s(X0),nbr_proc))),
% 98.39/12.87 inference(backward_demodulation,[status(thm)],[f2351,f11874])).
% 98.39/12.87 fof(f19304,plain,(
% 98.39/12.87 nbr_proc=s(host(sK10_skl))),
% 98.39/12.87 inference(backward_demodulation,[status(thm)],[f2351,f417])).
% 98.39/12.87 fof(f19496,definition,(
% 98.39/12.87 sQ533_spl <=> (nbr_proc=nbr_proc)),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ533_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f19498,plain,(
% 98.39/12.87 ~nbr_proc=nbr_proc|sQ533_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f19496])).
% 98.39/12.87 fof(f19501,plain,(
% 98.39/12.87 $false|sQ533_spl),
% 98.39/12.87 inference(trivial_equality_resolution,[status(thm)],[f19498])).
% 98.39/12.87 fof(f19502,plain,(
% 98.39/12.87 sQ533_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f19501])).
% 98.39/12.87 fof(f19587,definition,(
% 98.39/12.87 sQ536_spl <=> (leq(nbr_proc,s(host(sK10_skl))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f19589,plain,(
% 98.39/12.87 ~leq(nbr_proc,s(host(sK10_skl)))|sQ536_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f19587])).
% 98.39/12.87 fof(f19599,plain,(
% 98.39/12.87 leq(s(s(zero)),nbr_proc)),
% 98.39/12.87 inference(resolution,[status(thm)],[f19299,f74])).
% 98.39/12.87 fof(f20178,plain,(
% 98.39/12.87 s(s(nbr_proc))=s(nbr_proc)|~sQ514_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f2351,f18528])).
% 98.39/12.87 fof(f20242,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(s(s(nbr_proc))))))),s(nbr_proc))|~sQ514_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f20178,f484])).
% 98.39/12.87 fof(f20314,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(s(nbr_proc)))))),s(nbr_proc))|~sQ514_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f20178,f20242])).
% 98.39/12.87 fof(f20315,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(nbr_proc))))),s(nbr_proc))|~sQ514_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f20178,f20314])).
% 98.39/12.87 fof(f20316,plain,(
% 98.39/12.87 ~leq(s(s(s(s(nbr_proc)))),s(nbr_proc))|~sQ514_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f20178,f20315])).
% 98.39/12.87 fof(f20317,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),s(nbr_proc))|~sQ514_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f20178,f20316])).
% 98.39/12.87 fof(f20318,plain,(
% 98.39/12.87 ~leq(s(s(nbr_proc)),s(nbr_proc))|~sQ514_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f20178,f20317])).
% 98.39/12.87 fof(f20319,plain,(
% 98.39/12.87 ~leq(s(nbr_proc),s(nbr_proc))|~sQ514_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f20178,f20318])).
% 98.39/12.87 fof(f20320,plain,(
% 98.39/12.87 $false|~sQ514_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f20319,f192])).
% 98.39/12.87 fof(f20321,plain,(
% 98.39/12.87 ~sQ514_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f20320])).
% 98.39/12.87 fof(f20997,definition,(
% 98.39/12.87 ![X0]: (sQ570_spl <=> (tail(cons(X0,q_nil))=snoc(tail(q_nil),X0)))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ570_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f20998,plain,(
% 98.39/12.87 ![X0]: (tail(cons(X0,q_nil))=snoc(tail(q_nil),X0)|~sQ570_spl)),
% 98.39/12.87 inference(component_clause,[status(thm)],[f20997])).
% 98.39/12.87 fof(f21008,plain,(
% 98.39/12.87 ![X0]: (q_nil=snoc(tail(q_nil),X0)|~sQ570_spl)),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f128,f20998])).
% 98.39/12.87 fof(f21009,plain,(
% 98.39/12.87 $false|~sQ570_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f21008,f134])).
% 98.39/12.87 fof(f21010,plain,(
% 98.39/12.87 ~sQ570_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f21009])).
% 98.39/12.87 fof(f21086,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|sQ536_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f19589])).
% 98.39/12.87 fof(f21087,plain,(
% 98.39/12.87 $false|sQ536_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f21086,f192])).
% 98.39/12.87 fof(f21088,plain,(
% 98.39/12.87 sQ536_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f21087])).
% 98.39/12.87 fof(f21344,definition,(
% 98.39/12.87 sQ578_spl <=> (nbr_proc=s(s(s(nbr_proc))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f21345,plain,(
% 98.39/12.87 nbr_proc=s(s(s(nbr_proc)))|~sQ578_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f21344])).
% 98.39/12.87 fof(f21347,definition,(
% 98.39/12.87 sQ579_spl <=> (s(s(s(nbr_proc)))=s(nbr_proc))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ579_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f21348,plain,(
% 98.39/12.87 s(s(s(nbr_proc)))=s(nbr_proc)|~sQ579_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f21347])).
% 98.39/12.87 fof(f21351,definition,(
% 98.39/12.87 sQ580_spl <=> (s(nbr_proc)=s(s(s(s(nbr_proc)))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f21352,plain,(
% 98.39/12.87 s(nbr_proc)=s(s(s(s(nbr_proc))))|~sQ580_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f21351])).
% 98.39/12.87 fof(f21378,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ578_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f21345,f354])).
% 98.39/12.87 fof(f21467,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ578_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f21345,f21378])).
% 98.39/12.87 fof(f21468,plain,(
% 98.39/12.87 $false|~sQ578_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f21467,f192])).
% 98.39/12.87 fof(f21469,plain,(
% 98.39/12.87 ~sQ578_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f21468])).
% 98.39/12.87 fof(f21788,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(nbr_proc))))),s(nbr_proc))|~sQ579_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f21348,f354])).
% 98.39/12.87 fof(f21866,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),s(nbr_proc))|~sQ579_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f21348,f21788])).
% 98.39/12.87 fof(f21867,plain,(
% 98.39/12.87 ~leq(s(nbr_proc),s(nbr_proc))|~sQ579_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f21348,f21866])).
% 98.39/12.87 fof(f21868,plain,(
% 98.39/12.87 $false|~sQ579_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f21867,f192])).
% 98.39/12.87 fof(f21869,plain,(
% 98.39/12.87 ~sQ579_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f21868])).
% 98.39/12.87 fof(f22208,plain,(
% 98.39/12.87 ![X0]: (leq(host(sK10_skl),X0)|leq(X0,nbr_proc))),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f2351,f12658])).
% 98.39/12.87 fof(f22218,plain,(
% 98.39/12.87 leq(host(sK10_skl),nbr_proc)|leq(host(sK10_skl),nbr_proc)),
% 98.39/12.87 inference(resolution,[status(thm)],[f22208,f19297])).
% 98.39/12.87 fof(f22233,plain,(
% 98.39/12.87 sQ79_spl),
% 98.39/12.87 inference(split_clause,[status(thm)],[f22218,f1578])).
% 98.39/12.87 fof(f22666,plain,(
% 98.39/12.87 $false|~sQ37_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f2369,f75])).
% 98.39/12.87 fof(f22667,plain,(
% 98.39/12.87 ~sQ37_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f22666])).
% 98.39/12.87 fof(f22979,plain,(
% 98.39/12.87 ~leq(s(s(zero)),nbr_proc)|~sQ472_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f16736,f307])).
% 98.39/12.87 fof(f23050,plain,(
% 98.39/12.87 $false|~sQ472_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f22979,f19599])).
% 98.39/12.87 fof(f23051,plain,(
% 98.39/12.87 ~sQ472_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f23050])).
% 98.39/12.87 fof(f24273,definition,(
% 98.39/12.87 sQ632_spl <=> (host(sK10_skl)=s(s(s(nbr_proc))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f24274,plain,(
% 98.39/12.87 host(sK10_skl)=s(s(s(nbr_proc)))|~sQ632_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f24273])).
% 98.39/12.87 fof(f24279,definition,(
% 98.39/12.87 sQ633_spl <=> (host(sK10_skl)=s(host(sK10_skl)))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ633_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f24280,plain,(
% 98.39/12.87 host(sK10_skl)=s(host(sK10_skl))|~sQ633_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f24279])).
% 98.39/12.87 fof(f24283,plain,(
% 98.39/12.87 host(sK10_skl)=nbr_proc|~sQ633_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f24280])).
% 98.39/12.87 fof(f24284,plain,(
% 98.39/12.87 $false|~sQ633_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f24283,f19296])).
% 98.39/12.87 fof(f24285,plain,(
% 98.39/12.87 ~sQ633_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f24284])).
% 98.39/12.87 fof(f24892,definition,(
% 98.39/12.87 sQ647_spl <=> (s(s(s(s(s(host(sK10_skl))))))=nbr_proc)),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ647_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f24893,plain,(
% 98.39/12.87 s(s(s(s(s(host(sK10_skl))))))=nbr_proc|~sQ647_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f24892])).
% 98.39/12.87 fof(f24899,definition,(
% 98.39/12.87 sQ649_spl <=> (s(s(s(s(host(sK10_skl)))))=nbr_proc)),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f24900,plain,(
% 98.39/12.87 s(s(s(s(host(sK10_skl)))))=nbr_proc|~sQ649_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f24899])).
% 98.39/12.87 fof(f24907,definition,(
% 98.39/12.87 sQ651_spl <=> (s(s(s(host(sK10_skl))))=nbr_proc)),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f24908,plain,(
% 98.39/12.87 s(s(s(host(sK10_skl))))=nbr_proc|~sQ651_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f24907])).
% 98.39/12.87 fof(f24913,definition,(
% 98.39/12.87 sQ652_spl <=> (s(s(host(sK10_skl)))=nbr_proc)),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ652_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f24914,plain,(
% 98.39/12.87 s(s(host(sK10_skl)))=nbr_proc|~sQ652_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f24913])).
% 98.39/12.87 fof(f24933,plain,(
% 98.39/12.87 s(nbr_proc)=nbr_proc|~sQ652_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f24914])).
% 98.39/12.87 fof(f24934,plain,(
% 98.39/12.87 s(s(nbr_proc))=nbr_proc|~sQ651_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f24908])).
% 98.39/12.87 fof(f24935,plain,(
% 98.39/12.87 s(s(s(nbr_proc)))=nbr_proc|~sQ649_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f24900])).
% 98.39/12.87 fof(f24936,plain,(
% 98.39/12.87 s(s(s(s(nbr_proc))))=nbr_proc|~sQ647_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f24893])).
% 98.39/12.87 fof(f25131,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(s(nbr_proc)))))),nbr_proc)|~sQ652_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f24933,f484])).
% 98.39/12.87 fof(f25179,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(nbr_proc))))),nbr_proc)|~sQ652_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24933,f25131])).
% 98.39/12.87 fof(f25180,plain,(
% 98.39/12.87 ~leq(s(s(s(s(nbr_proc)))),nbr_proc)|~sQ652_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24933,f25179])).
% 98.39/12.87 fof(f25181,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ652_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24933,f25180])).
% 98.39/12.87 fof(f25182,plain,(
% 98.39/12.87 ~leq(s(s(nbr_proc)),nbr_proc)|~sQ652_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24933,f25181])).
% 98.39/12.87 fof(f25183,plain,(
% 98.39/12.87 ~leq(s(nbr_proc),nbr_proc)|~sQ652_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24933,f25182])).
% 98.39/12.87 fof(f25184,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ652_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24933,f25183])).
% 98.39/12.87 fof(f25185,plain,(
% 98.39/12.87 $false|~sQ652_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f25184,f192])).
% 98.39/12.87 fof(f25186,plain,(
% 98.39/12.87 ~sQ652_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f25185])).
% 98.39/12.87 fof(f25212,plain,(
% 98.39/12.87 ~leq(s(s(s(s(nbr_proc)))),nbr_proc)|~sQ651_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f24934,f354])).
% 98.39/12.87 fof(f25279,plain,(
% 98.39/12.87 ~leq(s(s(nbr_proc)),nbr_proc)|~sQ651_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24934,f25212])).
% 98.39/12.87 fof(f25280,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ651_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24934,f25279])).
% 98.39/12.87 fof(f25281,plain,(
% 98.39/12.87 $false|~sQ651_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f25280,f192])).
% 98.39/12.87 fof(f25282,plain,(
% 98.39/12.87 ~sQ651_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f25281])).
% 98.39/12.87 fof(f25473,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ649_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f24935,f354])).
% 98.39/12.87 fof(f25555,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ649_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24935,f25473])).
% 98.39/12.87 fof(f25556,plain,(
% 98.39/12.87 $false|~sQ649_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f25555,f192])).
% 98.39/12.87 fof(f25557,plain,(
% 98.39/12.87 ~sQ649_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f25556])).
% 98.39/12.87 fof(f25906,plain,(
% 98.39/12.87 ~leq(s(s(s(s(host(sK10_skl))))),nbr_proc)|~sQ632_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f24274,f484])).
% 98.39/12.87 fof(f25989,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ632_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f25906])).
% 98.39/12.87 fof(f25990,plain,(
% 98.39/12.87 ~leq(host(sK10_skl),nbr_proc)|~sQ632_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f24274,f25989])).
% 98.39/12.87 fof(f25991,plain,(
% 98.39/12.87 $false|~sQ632_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f25990,f76])).
% 98.39/12.87 fof(f25992,plain,(
% 98.39/12.87 ~sQ632_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f25991])).
% 98.39/12.87 fof(f26177,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ647_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f24936,f311])).
% 98.39/12.87 fof(f26263,plain,(
% 98.39/12.87 $false|~sQ647_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f26177,f192])).
% 98.39/12.87 fof(f26264,plain,(
% 98.39/12.87 ~sQ647_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f26263])).
% 98.39/12.87 fof(f27302,definition,(
% 98.39/12.87 sQ657_spl <=> (s(host(sK10_skl))=s(s(s(s(nbr_proc)))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f27303,plain,(
% 98.39/12.87 s(host(sK10_skl))=s(s(s(s(nbr_proc))))|~sQ657_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f27302])).
% 98.39/12.87 fof(f27320,plain,(
% 98.39/12.87 nbr_proc=s(s(s(s(nbr_proc))))|~sQ657_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f27303])).
% 98.39/12.87 fof(f27325,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ657_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f27320,f311])).
% 98.39/12.87 fof(f27414,plain,(
% 98.39/12.87 $false|~sQ657_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f27325,f192])).
% 98.39/12.87 fof(f27415,plain,(
% 98.39/12.87 ~sQ657_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f27414])).
% 98.39/12.87 fof(f27925,plain,(
% 98.39/12.87 nbr_proc=s(s(s(nbr_proc)))|~sQ418_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f14877])).
% 98.39/12.87 fof(f27930,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ418_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f27925,f354])).
% 98.39/12.87 fof(f28017,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ418_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f27925,f27930])).
% 98.39/12.87 fof(f28018,plain,(
% 98.39/12.87 $false|~sQ418_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f28017,f192])).
% 98.39/12.87 fof(f28019,plain,(
% 98.39/12.87 ~sQ418_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f28018])).
% 98.39/12.87 fof(f28243,definition,(
% 98.39/12.87 sQ676_spl <=> (zero=s(s(s(s(nbr_proc)))))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f28244,plain,(
% 98.39/12.87 zero=s(s(s(s(nbr_proc))))|~sQ676_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f28243])).
% 98.39/12.87 fof(f28271,plain,(
% 98.39/12.87 ~leq(s(zero),nbr_proc)|~sQ676_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f28244,f337])).
% 98.39/12.87 fof(f28365,plain,(
% 98.39/12.87 $false|~sQ676_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f28271,f75])).
% 98.39/12.87 fof(f28366,plain,(
% 98.39/12.87 ~sQ676_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f28365])).
% 98.39/12.87 fof(f28869,plain,(
% 98.39/12.87 nbr_proc=host(sK10_skl)|~sQ508_spl),
% 98.39/12.87 inference(resolution,[status(thm)],[f17946,f193])).
% 98.39/12.87 fof(f28881,plain,(
% 98.39/12.87 $false|~sQ508_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f28869,f19296])).
% 98.39/12.87 fof(f28882,plain,(
% 98.39/12.87 ~sQ508_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f28881])).
% 98.39/12.87 fof(f29180,definition,(
% 98.39/12.87 sQ686_spl <=> (leq(s(s(nbr_proc)),s(nbr_proc)))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ686_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f29181,plain,(
% 98.39/12.87 leq(s(s(nbr_proc)),s(nbr_proc))|~sQ686_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f29180])).
% 98.39/12.87 fof(f29203,plain,(
% 98.39/12.87 $false|~sQ686_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f29181,f191])).
% 98.39/12.87 fof(f29204,plain,(
% 98.39/12.87 ~sQ686_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f29203])).
% 98.39/12.87 fof(f30067,plain,(
% 98.39/12.87 $false|~sQ83_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f1647,f19296])).
% 98.39/12.87 fof(f30068,plain,(
% 98.39/12.87 ~sQ83_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f30067])).
% 98.39/12.87 fof(f30282,definition,(
% 98.39/12.87 sQ696_spl <=> (leq(s(s(host(sK10_skl))),nbr_proc))),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ696_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f30283,plain,(
% 98.39/12.87 leq(s(s(host(sK10_skl))),nbr_proc)|~sQ696_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f30282])).
% 98.39/12.87 fof(f30288,definition,(
% 98.39/12.87 sQ697_spl <=> (s(nbr_proc)=nbr_proc)),
% 98.39/12.87 introduced(definition,[new_symbols(definition,[sQ697_spl])],[split_symbol_definition])).
% 98.39/12.87 fof(f30289,plain,(
% 98.39/12.87 s(nbr_proc)=nbr_proc|~sQ697_spl),
% 98.39/12.87 inference(component_clause,[status(thm)],[f30288])).
% 98.39/12.87 fof(f30307,plain,(
% 98.39/12.87 leq(s(nbr_proc),nbr_proc)|~sQ696_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f30283])).
% 98.39/12.87 fof(f30308,plain,(
% 98.39/12.87 $false|~sQ696_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f30307,f191])).
% 98.39/12.87 fof(f30309,plain,(
% 98.39/12.87 ~sQ696_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f30308])).
% 98.39/12.87 fof(f30579,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(s(nbr_proc)))))),nbr_proc)|~sQ697_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f30289,f484])).
% 98.39/12.87 fof(f30649,plain,(
% 98.39/12.87 ~leq(s(s(s(s(s(nbr_proc))))),nbr_proc)|~sQ697_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f30289,f30579])).
% 98.39/12.87 fof(f30650,plain,(
% 98.39/12.87 ~leq(s(s(s(s(nbr_proc)))),nbr_proc)|~sQ697_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f30289,f30649])).
% 98.39/12.87 fof(f30651,plain,(
% 98.39/12.87 ~leq(s(s(s(nbr_proc))),nbr_proc)|~sQ697_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f30289,f30650])).
% 98.39/12.87 fof(f30652,plain,(
% 98.39/12.87 ~leq(s(s(nbr_proc)),nbr_proc)|~sQ697_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f30289,f30651])).
% 98.39/12.87 fof(f30653,plain,(
% 98.39/12.87 ~leq(s(nbr_proc),nbr_proc)|~sQ697_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f30289,f30652])).
% 98.39/12.87 fof(f30654,plain,(
% 98.39/12.87 ~leq(nbr_proc,nbr_proc)|~sQ697_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f30289,f30653])).
% 98.39/12.87 fof(f30655,plain,(
% 98.39/12.87 $false|~sQ697_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f30654,f192])).
% 98.39/12.87 fof(f30656,plain,(
% 98.39/12.87 ~sQ697_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f30655])).
% 98.39/12.87 fof(f32500,plain,(
% 98.39/12.87 ~leq(s(s(s(s(nbr_proc)))),s(nbr_proc))|~sQ580_spl),
% 98.39/12.87 inference(paramodulation,[status(thm)],[f21352,f354])).
% 98.39/12.87 fof(f32610,plain,(
% 98.39/12.87 ~leq(s(nbr_proc),s(nbr_proc))|~sQ580_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f21352,f32500])).
% 98.39/12.87 fof(f32611,plain,(
% 98.39/12.87 $false|~sQ580_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f32610,f192])).
% 98.39/12.87 fof(f32612,plain,(
% 98.39/12.87 ~sQ580_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f32611])).
% 98.39/12.87 fof(f32779,plain,(
% 98.39/12.87 ~leq(host(sK9_skl),nbr_proc)|sQ403_spl),
% 98.39/12.87 inference(forward_demodulation,[status(thm)],[f19304,f13917])).
% 98.39/12.87 fof(f32780,plain,(
% 98.39/12.87 $false|sQ403_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f32779,f76])).
% 98.39/12.87 fof(f32781,plain,(
% 98.39/12.87 sQ403_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f32780])).
% 98.39/12.87 fof(f32782,plain,(
% 98.39/12.87 $false|~sQ36_spl),
% 98.39/12.87 inference(forward_subsumption_resolution,[status(thm)],[f3088,f75])).
% 98.39/12.87 fof(f32783,plain,(
% 98.39/12.87 ~sQ36_spl),
% 98.39/12.87 inference(contradiction_clause,[status(thm)],[f32782])).
% 98.39/12.87 fof(f32950,plain,(
% 98.39/12.87 ~host(sK9_skl)=host(sK9_skl)|~sQ114_spl|~sQ17_spl),
% 98.39/12.87 inference(resolution,[status(thm)],[f6631,f2965])).
% 98.39/12.87 fof(f32951,plain,(
% 98.39/12.87 $false|~sQ114_spl|~sQ17_spl),
% 98.39/12.87 inference(trivial_equality_resolution,[status(thm)],[f32950])).
% 21.61/12.91 fof(f32952,plain,(
% 21.61/12.91 ~sQ114_spl|~sQ17_spl),
% 21.61/12.91 inference(contradiction_clause,[status(thm)],[f32951])).
% 21.61/12.91 fof(f33492,plain,(
% 21.61/12.91 ~host(sK10_skl)=host(sK10_skl)|~sQ91_spl|~sQ136_spl|~sQ113_spl),
% 21.61/12.91 inference(resolution,[status(thm)],[f5736,f5454])).
% 21.61/12.91 fof(f33495,plain,(
% 21.61/12.91 $false|~sQ91_spl|~sQ136_spl|~sQ113_spl),
% 21.61/12.91 inference(trivial_equality_resolution,[status(thm)],[f33492])).
% 21.61/12.91 fof(f33496,plain,(
% 21.61/12.91 ~sQ91_spl|~sQ136_spl|~sQ113_spl),
% 21.61/12.91 inference(contradiction_clause,[status(thm)],[f33495])).
% 21.61/12.91 fof(f33497,plain,(
% 21.61/12.91 $false),
% 21.61/12.91 inference(sat_refutation,[status(thm)],[f255,f455,f480,f482,f2209,f2524,f2527,f2567,f2569,f3042,f5436,f5450,f6770,f8165,f8206,f8315,f8534,f10581,f10759,f10775,f10821,f11638,f11973,f12870,f12887,f13841,f13941,f14166,f14601,f14768,f15358,f15564,f17154,f19502,f20321,f21010,f21088,f21469,f21869,f22233,f22667,f23051,f24285,f25186,f25282,f25557,f25992,f26264,f27415,f28019,f28366,f28882,f29204,f30068,f30309,f30656,f32612,f32781,f32783,f32952,f33496])).
% 21.61/12.91 % SZS output end CNFRefutation for theBenchmark.p
% 21.61/12.93 % Elapsed time: 12.545935 seconds
% 21.61/12.93 % CPU time: 99.187548 seconds
% 21.61/12.93 % Total memory used: 504.590 MB
% 21.61/12.93 % Net memory used: 424.012 MB
%------------------------------------------------------------------------------