%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV463+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 : n001.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 3.85s 1.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV463+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.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 08:58:14 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 3.85/1.16 % Refutation found
% 3.85/1.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.85/1.16 % SZS output start CNFRefutation for theBenchmark
% 3.85/1.16 fof(f4,axiom,(
% 3.85/1.16 leq(s(zero),nbr_proc) ),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f5,axiom,(
% 3.85/1.16 (! [P] : leq(host(P),nbr_proc) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f15,axiom,(
% 3.85/1.16 (! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f16,axiom,(
% 3.85/1.16 (! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f19,axiom,(
% 3.85/1.16 (! [X,Y] : m_Down(X) != m_Ldr(Y) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f21,axiom,(
% 3.85/1.16 (! [X,Y] : m_Down(X) != m_NormQ(Y) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f38,axiom,(
% 3.85/1.16 (! [Y,Q] : last(snoc(Q,Y)) = Y )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f42,axiom,(
% 3.85/1.16 (! [X,Q] : q_nil != cons(X,Q) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f44,axiom,(
% 3.85/1.16 (! [X] : cons(X,q_nil) = snoc(q_nil,X) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f48,axiom,(
% 3.85/1.16 (! [X,Y,Q] :( elem(X,snoc(Q,Y))<=> ( X = Y| elem(X,Q) ) ) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f59,axiom,(
% 3.85/1.16 (! [X] : ~ leq(s(X),X) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f60,axiom,(
% 3.85/1.16 (! [X] : leq(X,X) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f61,axiom,(
% 3.85/1.16 (! [X,Y] :( leq(X,Y)| leq(Y,X) ) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f62,axiom,(
% 3.85/1.16 (! [X,Y] :( ( leq(X,Y)& leq(Y,X) )<=> X = Y ) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f63,axiom,(
% 3.85/1.16 (! [X,Y,Z] :( ( leq(X,Y)& leq(Y,Z) )=> leq(X,Z) ) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f67,conjecture,(
% 3.85/1.16 (! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( elem(m_Down(Pid0),queue(host(Z)))=> host(Pid0) != host(Z) ))& (! [Z,Pid0] :( elem(m_Halt(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid20,Pid0] :( elem(m_Ack(Pid0,Z),queue(host(Pid20)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0))) )=> leq(host(Z),index(pendack,host(Pid0))) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = elec_1 )=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid20) = host(Z) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) ))& (! [Z,Pid20,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Z))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Pid20)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid0) = nbr_proc& host(Pid0) = host(Pid30)& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid30),queue(host(Z))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Pid30) = index(pendack,host(Pid0))& host(Pid20) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Ack(W,Y),V) )=> ( setIn(X,alive)=> ( ( index(elid,host(X)) = W& index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> ( leq(nbr_proc,index(pendack,host(X)))=> (! [Z] :( ( setIn(host(Z),index(acks,host(X)))| host(Z) = host(Y) )=> (! [V0] :( host(X) != host(V0)=> (! [W0,X0,Y0] :( host(Z) = host(Y0)=> ( host(X) != host(Y0)=> ( ( setIn(Y0,alive)& leq(nbr_proc,s(index(pendack,host(Y0))))& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))& index(status,host(Y0)) = elec_2& host(W0) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(V0,alive)& index(ldr,host(V0)) = host(V0)& index(status,host(V0)) = norm ) ) ) ) )) )) )) ) ) ) )),
% 3.85/1.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/1.16 fof(f68,negated_conjecture,(
% 3.85/1.16 ~((! [V,W,X,Y] :( ( (! [Z,Pid0] :( elem(m_Ldr(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( elem(m_Down(Pid0),queue(host(Z)))=> host(Pid0) != host(Z) ))& (! [Z,Pid0] :( elem(m_Halt(Pid0),queue(host(Z)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid20,Pid0] :( elem(m_Ack(Pid0,Z),queue(host(Pid20)))=> ~ leq(host(Z),host(Pid0)) ))& (! [Z,Pid0] :( ( Pid0 != Z& host(Pid0) = host(Z) )=> ( ~ setIn(Z,alive)| ~ setIn(Pid0,alive) ) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& elem(m_Ack(Pid0,Z),queue(host(Pid0))) )=> leq(host(Z),index(pendack,host(Pid0))) ))& (! [Z,Pid0] :( ( setIn(Pid0,alive)& index(status,host(Pid0)) = elec_1 )=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) ))& (! [Z] :( ( ( index(status,host(Z)) = elec_1| index(status,host(Z)) = elec_2 )& setIn(Z,alive) )=> index(elid,host(Z)) = Z ))& (! [Z,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid20) = host(Z) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> leq(index(pendack,host(Pid0)),host(Z)) ))& (! [Z,Pid20,Pid0] :( ( setIn(Z,alive)& setIn(Pid0,alive)& host(Pid0) = host(Pid20)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) ))& (! [Z,Pid0] :( ( ~ leq(host(Z),host(Pid0))& setIn(Z,alive)& setIn(Pid0,alive)& index(status,host(Z)) = elec_2& index(status,host(Pid0)) = elec_2 )=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) ))& (! [Z,Pid20,Pid0] :( ( ~ leq(index(pendack,host(Pid0)),host(Z))& setIn(Pid0,alive)& elem(m_Halt(Pid0),queue(host(Pid20)))& index(status,host(Pid0)) = elec_2 )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( (! [V0] :( ( ~ leq(host(Pid0),V0)& leq(s(zero),V0) )=> ( setIn(V0,index(down,host(Pid0)))| V0 = host(Pid20) ) ))& elem(m_Down(Pid20),queue(host(Pid0)))& host(Pid0) = nbr_proc& host(Pid0) = host(Pid30)& index(status,host(Pid0)) = elec_1 )=> ~ ( setIn(Z,alive)& elem(m_Down(Pid30),queue(host(Z))) ) ))& (! [Z,Pid30,Pid20,Pid0] :( ( setIn(Pid0,alive)& elem(m_Down(Pid20),queue(host(Pid0)))& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))& leq(nbr_proc,s(index(pendack,host(Pid0))))& index(status,host(Pid0)) = elec_2& host(Pid30) = index(pendack,host(Pid0))& host(Pid20) = s(index(pendack,host(Pid0))) )=> ~ ( setIn(Z,alive)& index(ldr,host(Z)) = host(Z)& index(status,host(Z)) = norm ) ))& queue(host(X)) = cons(m_Ack(W,Y),V) )=> ( setIn(X,alive)=> ( ( index(elid,host(X)) = W& index(status,host(X)) = elec_2& host(Y) = index(pendack,host(X)) )=> ( leq(nbr_proc,index(pendack,host(X)))=> (! [Z] :( ( setIn(host(Z),index(acks,host(X)))| host(Z) = host(Y) )=> (! [V0] :( host(X) != host(V0)=> (! [W0,X0,Y0] :( host(Z) = host(Y0)=> ( host(X) != host(Y0)=> ( ( setIn(Y0,alive)& leq(nbr_proc,s(index(pendack,host(Y0))))& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))& index(status,host(Y0)) = elec_2& host(W0) = index(pendack,host(Y0))& host(X0) = s(index(pendack,host(Y0))) )=> ~ ( setIn(V0,alive)& index(ldr,host(V0)) = host(V0)& index(status,host(V0)) = norm ) ) ) ) )) )) )) ) ) ) ))),
% 3.85/1.16 inference(negated_conjecture,[status(cth)],[f67])).
% 3.85/1.16 fof(f75,plain,(
% 3.85/1.16 leq(s(zero),nbr_proc)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f4])).
% 3.85/1.16 fof(f76,plain,(
% 3.85/1.16 ![X0]: (leq(host(X0),nbr_proc))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f5])).
% 3.85/1.16 fof(f86,plain,(
% 3.85/1.16 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_Ldr(X2))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f15])).
% 3.85/1.16 fof(f87,plain,(
% 3.85/1.16 ![X0,X1,X2]: (~m_Ack(X0,X1)=m_NormQ(X2))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f16])).
% 3.85/1.16 fof(f90,plain,(
% 3.85/1.16 ![X0,X1]: (~m_Down(X0)=m_Ldr(X1))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f19])).
% 3.85/1.16 fof(f92,plain,(
% 3.85/1.16 ![X0,X1]: (~m_Down(X0)=m_NormQ(X1))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f21])).
% 3.85/1.16 fof(f129,plain,(
% 3.85/1.16 ![X0,X1]: (last(snoc(X0,X1))=X1)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f38])).
% 3.85/1.16 fof(f133,plain,(
% 3.85/1.16 ![X0,X1]: (~q_nil=cons(X0,X1))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f42])).
% 3.85/1.16 fof(f135,plain,(
% 3.85/1.16 ![X0]: (cons(X0,q_nil)=snoc(q_nil,X0))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f44])).
% 3.85/1.16 fof(f143,plain,(
% 3.85/1.16 ![X,Y,Q]: ((~elem(X,snoc(Q,Y))|(X=Y|elem(X,Q)))&(elem(X,snoc(Q,Y))|(~X=Y&~elem(X,Q))))),
% 3.85/1.16 inference(NNF_transformation,[status(thm)],[f48])).
% 3.85/1.16 fof(f144,plain,(
% 3.85/1.16 (![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))))),
% 3.85/1.16 inference(miniscoping,[status(thm)],[f143])).
% 3.85/1.16 fof(f145,plain,(
% 3.85/1.16 ![X0,X1,X2]: (~elem(X0,snoc(X1,X2))|X0=X2|elem(X0,X1))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f144])).
% 3.85/1.16 fof(f191,plain,(
% 3.85/1.16 ![X0]: (~leq(s(X0),X0))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f59])).
% 3.85/1.16 fof(f192,plain,(
% 3.85/1.16 ![X0]: (leq(X0,X0))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f60])).
% 3.85/1.16 fof(f193,plain,(
% 3.85/1.16 ![X0,X1]: (leq(X0,X1)|leq(X1,X0))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f61])).
% 3.85/1.16 fof(f194,plain,(
% 3.85/1.16 ![X,Y]: (((~leq(X,Y)|~leq(Y,X))|X=Y)&((leq(X,Y)&leq(Y,X))|~X=Y))),
% 3.85/1.16 inference(NNF_transformation,[status(thm)],[f62])).
% 3.85/1.16 fof(f195,plain,(
% 3.85/1.16 (![X,Y]: ((~leq(X,Y)|~leq(Y,X))|X=Y))&(![X,Y]: ((leq(X,Y)&leq(Y,X))|~X=Y))),
% 3.85/1.16 inference(miniscoping,[status(thm)],[f194])).
% 3.85/1.16 fof(f196,plain,(
% 3.85/1.16 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|X0=X1)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f195])).
% 3.85/1.16 fof(f199,plain,(
% 3.85/1.16 ![X,Y,Z]: ((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))),
% 3.85/1.16 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 3.85/1.16 fof(f200,plain,(
% 3.85/1.16 ![X,Z]: ((![Y]: (~leq(X,Y)|~leq(Y,Z)))|leq(X,Z))),
% 3.85/1.16 inference(miniscoping,[status(thm)],[f199])).
% 3.85/1.16 fof(f201,plain,(
% 3.85/1.16 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|leq(X0,X2))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f200])).
% 3.85/1.16 fof(f212,plain,(
% 3.85/1.16 (?[V,W,X,Y]: (((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid20,Pid0]: (~elem(m_Ack(Pid0,Z),queue(host(Pid20)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|leq(host(Z),index(pendack,host(Pid0))))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_1)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z,Pid20,Pid0]: (((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid20)=host(Z))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20,Pid0]: (((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~leq(index(pendack,host(Z)),index(pendack,host(Pid0))))))&(![Z,Pid20,Pid0]: ((((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|~elem(m_Halt(Pid0),queue(host(Pid20))))|~index(status,host(Pid0))=elec_2)|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid30,Pid20,Pid0]: ((((((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~elem(m_Down(Pid20),queue(host(Pid0))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1)|(~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z)))))))&(![Z,Pid30,Pid20,Pid0]: (((((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~elem(m_Ack(Pid0,Pid30),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Pid30)=index(pendack,host(Pid0)))|~host(Pid20)=s(index(pendack,host(Pid0))))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(X))=cons(m_Ack(W,Y),V))&(setIn(X,alive)&(((index(elid,host(X))=W&index(status,host(X))=elec_2)&host(Y)=index(pendack,host(X)))&(leq(nbr_proc,index(pendack,host(X)))&(?[Z]: ((setIn(host(Z),index(acks,host(X)))|host(Z)=host(Y))&(?[V0]: (~host(X)=host(V0)&(?[W0,X0,Y0]: (host(Z)=host(Y0)&(~host(X)=host(Y0)&(((((((setIn(Y0,alive)&leq(nbr_proc,s(index(pendack,host(Y0)))))&elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X))))&elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X))))&index(status,host(Y0))=elec_2)&host(W0)=index(pendack,host(Y0)))&host(X0)=s(index(pendack,host(Y0))))&((setIn(V0,alive)&index(ldr,host(V0))=host(V0))&index(status,host(V0))=norm))))))))))))))),
% 3.85/1.16 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 3.85/1.16 fof(f213,plain,(
% 3.85/1.16 ?[W,X,Y]: (((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((![Pid20]: ~elem(m_Ack(Pid0,Z),queue(host(Pid20))))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|leq(host(Z),index(pendack,host(Pid0))))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_1)|(![Z]: ~elem(m_Ack(Pid0,Z),queue(host(Pid0)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z]: ((![Pid20]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid20)=host(Z)))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20]: ((![Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~leq(index(pendack,host(Z)),index(pendack,host(Pid0))))))&(![Z]: ((![Pid0]: (((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|(![Pid20]: ~elem(m_Halt(Pid0),queue(host(Pid20)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Pid30]: ((![Pid0]: ((((![Pid20]: ((?[V0]: ((~leq(host(Pid0),V0)&leq(s(zero),V0))&(~setIn(V0,index(down,host(Pid0)))&~V0=host(Pid20))))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z))))))))&((![Pid20,Pid0]: ((![Pid30]: (((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~elem(m_Ack(Pid0,Pid30),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Pid30)=index(pendack,host(Pid0))))|~host(Pid20)=s(index(pendack,host(Pid0)))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(?[V]: queue(host(X))=cons(m_Ack(W,Y),V)))&(setIn(X,alive)&(((index(elid,host(X))=W&index(status,host(X))=elec_2)&host(Y)=index(pendack,host(X)))&(leq(nbr_proc,index(pendack,host(X)))&(?[Z]: ((setIn(host(Z),index(acks,host(X)))|host(Z)=host(Y))&(?[V0]: (~host(X)=host(V0)&(?[Y0]: (host(Z)=host(Y0)&(~host(X)=host(Y0)&((?[X0]: ((?[W0]: (((((setIn(Y0,alive)&leq(nbr_proc,s(index(pendack,host(Y0)))))&elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X))))&elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X))))&index(status,host(Y0))=elec_2)&host(W0)=index(pendack,host(Y0))))&host(X0)=s(index(pendack,host(Y0)))))&((setIn(V0,alive)&index(ldr,host(V0))=host(V0))&index(status,host(V0))=norm)))))))))))))),
% 3.85/1.16 inference(miniscoping,[status(thm)],[f212])).
% 3.85/1.16 fof(f214,plain,(
% 3.85/1.16 (((((((((((((((((![Z,Pid0]: (~elem(m_Ldr(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0))))&(![Z,Pid0]: (~elem(m_Down(Pid0),queue(host(Z)))|~host(Pid0)=host(Z))))&(![Z,Pid0]: (~elem(m_Halt(Pid0),queue(host(Z)))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((![Pid20]: ~elem(m_Ack(Pid0,Z),queue(host(Pid20))))|~leq(host(Z),host(Pid0)))))&(![Z,Pid0]: ((Pid0=Z|~host(Pid0)=host(Z))|(~setIn(Z,alive)|~setIn(Pid0,alive)))))&(![Z,Pid0]: ((~setIn(Pid0,alive)|~elem(m_Ack(Pid0,Z),queue(host(Pid0))))|leq(host(Z),index(pendack,host(Pid0))))))&(![Pid0]: ((~setIn(Pid0,alive)|~index(status,host(Pid0))=elec_1)|(![Z]: ~elem(m_Ack(Pid0,Z),queue(host(Pid0)))))))&(![Z]: (((~index(status,host(Z))=elec_1&~index(status,host(Z))=elec_2)|~setIn(Z,alive))|index(elid,host(Z))=Z)))&(![Z]: ((![Pid20]: ((![Pid0]: (~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid20)=host(Z)))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|leq(index(pendack,host(Pid0)),host(Z)))))&(![Z,Pid20]: ((![Pid0]: ((((~setIn(Z,alive)|~setIn(Pid0,alive))|~host(Pid0)=host(Pid20))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2))|~elem(m_Ack(Z,Pid20),queue(host(Z))))))&(![Z,Pid0]: (((((leq(host(Z),host(Pid0))|~setIn(Z,alive))|~setIn(Pid0,alive))|~index(status,host(Z))=elec_2)|~index(status,host(Pid0))=elec_2)|~leq(index(pendack,host(Z)),index(pendack,host(Pid0))))))&(![Z]: ((![Pid0]: (((leq(index(pendack,host(Pid0)),host(Z))|~setIn(Pid0,alive))|(![Pid20]: ~elem(m_Halt(Pid0),queue(host(Pid20)))))|~index(status,host(Pid0))=elec_2))|((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&(![Pid30]: ((![Pid0]: ((((![Pid20]: (((~leq(host(Pid0),sK7_skl(Pid20,Pid0,Pid30))&leq(s(zero),sK7_skl(Pid20,Pid0,Pid30)))&(~setIn(sK7_skl(Pid20,Pid0,Pid30),index(down,host(Pid0)))&~sK7_skl(Pid20,Pid0,Pid30)=host(Pid20)))|~elem(m_Down(Pid20),queue(host(Pid0)))))|~host(Pid0)=nbr_proc)|~host(Pid0)=host(Pid30))|~index(status,host(Pid0))=elec_1))|(![Z]: (~setIn(Z,alive)|~elem(m_Down(Pid30),queue(host(Z))))))))&((![Pid20,Pid0]: ((![Pid30]: (((((~setIn(Pid0,alive)|~elem(m_Down(Pid20),queue(host(Pid0))))|~elem(m_Ack(Pid0,Pid30),queue(host(Pid0))))|~leq(nbr_proc,s(index(pendack,host(Pid0)))))|~index(status,host(Pid0))=elec_2)|~host(Pid30)=index(pendack,host(Pid0))))|~host(Pid20)=s(index(pendack,host(Pid0)))))|(![Z]: ((~setIn(Z,alive)|~index(ldr,host(Z))=host(Z))|~index(status,host(Z))=norm))))&queue(host(sK5_skl))=cons(m_Ack(sK4_skl,sK6_skl),sK8_skl))&(setIn(sK5_skl,alive)&(((index(elid,host(sK5_skl))=sK4_skl&index(status,host(sK5_skl))=elec_2)&host(sK6_skl)=index(pendack,host(sK5_skl)))&(leq(nbr_proc,index(pendack,host(sK5_skl)))&((setIn(host(sK9_skl),index(acks,host(sK5_skl)))|host(sK9_skl)=host(sK6_skl))&(~host(sK5_skl)=host(sK10_skl)&(host(sK9_skl)=host(sK11_skl)&(~host(sK5_skl)=host(sK11_skl)&(((((((setIn(sK11_skl,alive)&leq(nbr_proc,s(index(pendack,host(sK11_skl)))))&elem(m_Down(sK12_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl))))&elem(m_Ack(sK11_skl,sK13_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl))))&index(status,host(sK11_skl))=elec_2)&host(sK13_skl)=index(pendack,host(sK11_skl)))&host(sK12_skl)=s(index(pendack,host(sK11_skl))))&((setIn(sK10_skl,alive)&index(ldr,host(sK10_skl))=host(sK10_skl))&index(status,host(sK10_skl))=norm))))))))))),
% 3.85/1.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(W,sK4_skl),skolemize(X,sK5_skl),skolemize(Y,sK6_skl),skolemize(V0,sK7_skl(Pid20,Pid0,Pid30)),skolemize(V,sK8_skl),skolemize(Z,sK9_skl),skolemize(V0,sK10_skl),skolemize(Y0,sK11_skl),skolemize(X0,sK12_skl),skolemize(W0,sK13_skl)],[f213])).
% 3.85/1.16 fof(f233,plain,(
% 3.85/1.16 ![X0,X1,X2,X3]: (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))|~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f242,plain,(
% 3.85/1.16 host(sK9_skl)=host(sK11_skl)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f244,plain,(
% 3.85/1.16 setIn(sK11_skl,alive)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f245,plain,(
% 3.85/1.16 leq(nbr_proc,s(index(pendack,host(sK11_skl))))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f246,plain,(
% 3.85/1.16 elem(m_Down(sK12_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl)))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f247,plain,(
% 3.85/1.16 elem(m_Ack(sK11_skl,sK13_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl)))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f248,plain,(
% 3.85/1.16 index(status,host(sK11_skl))=elec_2),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f249,plain,(
% 3.85/1.16 host(sK13_skl)=index(pendack,host(sK11_skl))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f250,plain,(
% 3.85/1.16 host(sK12_skl)=s(index(pendack,host(sK11_skl)))),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f251,plain,(
% 3.85/1.16 setIn(sK10_skl,alive)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f252,plain,(
% 3.85/1.16 index(ldr,host(sK10_skl))=host(sK10_skl)),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f253,plain,(
% 3.85/1.16 index(status,host(sK10_skl))=norm),
% 3.85/1.16 inference(cnf_transformation,[status(thm)],[f214])).
% 3.85/1.16 fof(f254,definition,(
% 3.85/1.16 ![X0,X1,X2]: (sQ0_spl <=> (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f255,plain,(
% 3.85/1.16 ![X0,X1,X2]: (~setIn(X0,alive)|~elem(m_Down(X1),queue(host(X0)))|~elem(m_Ack(X0,X2),queue(host(X0)))|~leq(nbr_proc,s(index(pendack,host(X0))))|~index(status,host(X0))=elec_2|~host(X2)=index(pendack,host(X0))|~host(X1)=s(index(pendack,host(X0)))|~sQ0_spl)),
% 3.85/1.16 inference(component_clause,[status(thm)],[f254])).
% 3.85/1.16 fof(f257,definition,(
% 3.85/1.16 ![X3]: (sQ1_spl <=> (~setIn(X3,alive)|~index(ldr,host(X3))=host(X3)|~index(status,host(X3))=norm))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f258,plain,(
% 3.85/1.16 ![X0]: (~setIn(X0,alive)|~index(ldr,host(X0))=host(X0)|~index(status,host(X0))=norm|~sQ1_spl)),
% 3.85/1.16 inference(component_clause,[status(thm)],[f257])).
% 3.85/1.16 fof(f260,plain,(
% 3.85/1.16 sQ0_spl|sQ1_spl),
% 3.85/1.16 inference(split_clause,[status(thm)],[f233,f254,f257])).
% 3.85/1.16 fof(f308,definition,(
% 3.85/1.16 sQ6_spl <=> (setIn(sK11_skl,alive))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f310,plain,(
% 3.85/1.16 ~setIn(sK11_skl,alive)|sQ6_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f308])).
% 3.85/1.16 fof(f315,plain,(
% 3.85/1.16 $false|sQ6_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f310,f244])).
% 3.85/1.16 fof(f316,plain,(
% 3.85/1.16 sQ6_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f315])).
% 3.85/1.16 fof(f318,plain,(
% 3.85/1.16 ![X0]: (leq(X0,s(X0)))),
% 3.85/1.16 inference(resolution,[status(thm)],[f193,f191])).
% 3.85/1.16 fof(f451,plain,(
% 3.85/1.16 index(status,host(sK9_skl))=elec_2),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f248])).
% 3.85/1.16 fof(f459,definition,(
% 3.85/1.16 sQ19_spl <=> (index(status,host(sK11_skl))=elec_2)),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f461,plain,(
% 3.85/1.16 ~index(status,host(sK11_skl))=elec_2|sQ19_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f459])).
% 3.85/1.16 fof(f492,plain,(
% 3.85/1.16 ![X0,X1]: (~leq(s(X0),X1)|leq(X0,X1))),
% 3.85/1.16 inference(resolution,[status(thm)],[f201,f318])).
% 3.85/1.16 fof(f494,plain,(
% 3.85/1.16 ![X0,X1,X2]: (~leq(X0,X1)|leq(X2,X1)|leq(X0,X2))),
% 3.85/1.16 inference(resolution,[status(thm)],[f201,f193])).
% 3.85/1.16 fof(f585,plain,(
% 3.85/1.16 ~index(status,host(sK9_skl))=elec_2|sQ19_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f461])).
% 3.85/1.16 fof(f586,plain,(
% 3.85/1.16 ~elec_2=elec_2|sQ19_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f451,f585])).
% 3.85/1.16 fof(f587,plain,(
% 3.85/1.16 $false|sQ19_spl),
% 3.85/1.16 inference(trivial_equality_resolution,[status(thm)],[f586])).
% 3.85/1.16 fof(f588,plain,(
% 3.85/1.16 sQ19_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f587])).
% 3.85/1.16 fof(f789,plain,(
% 3.85/1.16 leq(nbr_proc,s(index(pendack,host(sK9_skl))))),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f245])).
% 3.85/1.16 fof(f806,plain,(
% 3.85/1.16 elem(m_Down(sK12_skl),snoc(queue(host(sK9_skl)),m_Ldr(sK5_skl)))),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f246])).
% 3.85/1.16 fof(f807,plain,(
% 3.85/1.16 m_Down(sK12_skl)=m_Ldr(sK5_skl)|elem(m_Down(sK12_skl),queue(host(sK9_skl)))),
% 3.85/1.16 inference(resolution,[status(thm)],[f806,f145])).
% 3.85/1.16 fof(f810,definition,(
% 3.85/1.16 sQ50_spl <=> (m_Down(sK12_skl)=m_Ldr(sK5_skl))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f811,plain,(
% 3.85/1.16 m_Down(sK12_skl)=m_Ldr(sK5_skl)|~sQ50_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f810])).
% 3.85/1.16 fof(f813,definition,(
% 3.85/1.16 sQ51_spl <=> (elem(m_Down(sK12_skl),queue(host(sK9_skl))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f814,plain,(
% 3.85/1.16 elem(m_Down(sK12_skl),queue(host(sK9_skl)))|~sQ51_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f813])).
% 3.85/1.16 fof(f816,plain,(
% 3.85/1.16 sQ50_spl|sQ51_spl),
% 3.85/1.16 inference(split_clause,[status(thm)],[f807,f810,f813])).
% 3.85/1.16 fof(f817,plain,(
% 3.85/1.16 $false|~sQ50_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f811,f90])).
% 3.85/1.16 fof(f818,plain,(
% 3.85/1.16 ~sQ50_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f817])).
% 3.85/1.16 fof(f896,plain,(
% 3.85/1.16 elem(m_Ack(sK11_skl,sK13_skl),snoc(queue(host(sK9_skl)),m_Ldr(sK5_skl)))),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f247])).
% 3.85/1.16 fof(f897,plain,(
% 3.85/1.16 m_Ack(sK11_skl,sK13_skl)=m_Ldr(sK5_skl)|elem(m_Ack(sK11_skl,sK13_skl),queue(host(sK9_skl)))),
% 3.85/1.16 inference(resolution,[status(thm)],[f896,f145])).
% 3.85/1.16 fof(f900,definition,(
% 3.85/1.16 sQ65_spl <=> (m_Ack(sK11_skl,sK13_skl)=m_Ldr(sK5_skl))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f901,plain,(
% 3.85/1.16 m_Ack(sK11_skl,sK13_skl)=m_Ldr(sK5_skl)|~sQ65_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f900])).
% 3.85/1.16 fof(f903,definition,(
% 3.85/1.16 sQ66_spl <=> (elem(m_Ack(sK11_skl,sK13_skl),queue(host(sK9_skl))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f904,plain,(
% 3.85/1.16 elem(m_Ack(sK11_skl,sK13_skl),queue(host(sK9_skl)))|~sQ66_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f903])).
% 3.85/1.16 fof(f906,plain,(
% 3.85/1.16 sQ65_spl|sQ66_spl),
% 3.85/1.16 inference(split_clause,[status(thm)],[f897,f900,f903])).
% 3.85/1.16 fof(f907,plain,(
% 3.85/1.16 $false|~sQ65_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f901,f86])).
% 3.85/1.16 fof(f908,plain,(
% 3.85/1.16 ~sQ65_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f907])).
% 3.85/1.16 fof(f909,plain,(
% 3.85/1.16 leq(nbr_proc,s(host(sK13_skl)))),
% 3.85/1.16 inference(backward_demodulation,[status(thm)],[f910,f789])).
% 3.85/1.16 fof(f910,plain,(
% 3.85/1.16 host(sK13_skl)=index(pendack,host(sK9_skl))),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f249])).
% 3.85/1.16 fof(f930,plain,(
% 3.85/1.16 host(sK12_skl)=s(index(pendack,host(sK9_skl)))),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f250])).
% 3.85/1.16 fof(f931,plain,(
% 3.85/1.16 host(sK12_skl)=s(host(sK13_skl))),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f910,f930])).
% 3.85/1.16 fof(f942,plain,(
% 3.85/1.16 ![X0,X1]: (~setIn(sK11_skl,alive)|~elem(m_Down(X0),queue(host(sK9_skl)))|~elem(m_Ack(sK11_skl,X1),queue(host(sK11_skl)))|~leq(nbr_proc,s(index(pendack,host(sK11_skl))))|~index(status,host(sK11_skl))=elec_2|~host(X1)=index(pendack,host(sK11_skl))|~host(X0)=s(index(pendack,host(sK11_skl)))|~sQ0_spl)),
% 3.85/1.16 inference(paramodulation,[status(thm)],[f242,f255])).
% 3.85/1.16 fof(f953,definition,(
% 3.85/1.16 ![X0]: (sQ74_spl <=> (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=s(index(pendack,host(sK11_skl)))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f954,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=s(index(pendack,host(sK11_skl)))|~sQ74_spl)),
% 3.85/1.16 inference(component_clause,[status(thm)],[f953])).
% 3.85/1.16 fof(f956,definition,(
% 3.85/1.16 ![X1]: (sQ75_spl <=> (~elem(m_Ack(sK11_skl,X1),queue(host(sK11_skl)))|~host(X1)=index(pendack,host(sK11_skl))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f957,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Ack(sK11_skl,X0),queue(host(sK11_skl)))|~host(X0)=index(pendack,host(sK11_skl))|~sQ75_spl)),
% 3.85/1.16 inference(component_clause,[status(thm)],[f956])).
% 3.85/1.16 fof(f959,definition,(
% 3.85/1.16 sQ76_spl <=> (leq(nbr_proc,s(index(pendack,host(sK11_skl)))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f961,plain,(
% 3.85/1.16 ~leq(nbr_proc,s(index(pendack,host(sK11_skl))))|sQ76_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f959])).
% 3.85/1.16 fof(f962,plain,(
% 3.85/1.16 ~sQ6_spl|sQ74_spl|sQ75_spl|~sQ76_spl|~sQ19_spl|~sQ0_spl),
% 3.85/1.16 inference(split_clause,[status(thm)],[f942,f308,f953,f956,f959,f459,f254])).
% 3.85/1.16 fof(f963,plain,(
% 3.85/1.16 ~leq(nbr_proc,s(index(pendack,host(sK9_skl))))|sQ76_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f961])).
% 3.85/1.16 fof(f964,plain,(
% 3.85/1.16 ~leq(nbr_proc,s(host(sK13_skl)))|sQ76_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f910,f963])).
% 3.85/1.16 fof(f965,plain,(
% 3.85/1.16 ~leq(nbr_proc,host(sK12_skl))|sQ76_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f931,f964])).
% 3.85/1.16 fof(f1010,plain,(
% 3.85/1.16 leq(nbr_proc,host(sK12_skl))),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f931,f909])).
% 3.85/1.16 fof(f1011,plain,(
% 3.85/1.16 $false|sQ76_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f1010,f965])).
% 3.85/1.16 fof(f1012,plain,(
% 3.85/1.16 sQ76_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f1011])).
% 3.85/1.16 fof(f1013,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=s(index(pendack,host(sK9_skl)))|~sQ74_spl)),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f954])).
% 3.85/1.16 fof(f1014,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=s(host(sK13_skl))|~sQ74_spl)),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f910,f1013])).
% 3.85/1.16 fof(f1015,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=host(sK12_skl)|~sQ74_spl)),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f931,f1014])).
% 3.85/1.16 fof(f1035,plain,(
% 3.85/1.16 ~leq(host(sK12_skl),nbr_proc)|nbr_proc=host(sK12_skl)),
% 3.85/1.16 inference(resolution,[status(thm)],[f1010,f196])).
% 3.85/1.16 fof(f1036,definition,(
% 3.85/1.16 sQ84_spl <=> (leq(host(sK12_skl),nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f1038,plain,(
% 3.85/1.16 ~leq(host(sK12_skl),nbr_proc)|sQ84_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f1036])).
% 3.85/1.16 fof(f1039,definition,(
% 3.85/1.16 sQ85_spl <=> (nbr_proc=host(sK12_skl))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f1040,plain,(
% 3.85/1.16 nbr_proc=host(sK12_skl)|~sQ85_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f1039])).
% 3.85/1.16 fof(f1042,plain,(
% 3.85/1.16 ~sQ84_spl|sQ85_spl),
% 3.85/1.16 inference(split_clause,[status(thm)],[f1035,f1036,f1039])).
% 3.85/1.16 fof(f1043,plain,(
% 3.85/1.16 $false|sQ84_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f1038,f76])).
% 3.85/1.16 fof(f1044,plain,(
% 3.85/1.16 sQ84_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f1043])).
% 3.85/1.16 fof(f1169,plain,(
% 3.85/1.16 leq(zero,nbr_proc)),
% 3.85/1.16 inference(resolution,[status(thm)],[f492,f75])).
% 3.85/1.16 fof(f1335,plain,(
% 3.85/1.16 ![X0]: (~leq(nbr_proc,X0)|leq(zero,X0))),
% 3.85/1.16 inference(resolution,[status(thm)],[f1169,f201])).
% 3.85/1.16 fof(f1775,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Ack(sK11_skl,X0),queue(host(sK9_skl)))|~host(X0)=index(pendack,host(sK11_skl))|~sQ75_spl)),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f957])).
% 3.85/1.16 fof(f1776,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Ack(sK11_skl,X0),queue(host(sK9_skl)))|~host(X0)=index(pendack,host(sK9_skl))|~sQ75_spl)),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f242,f1775])).
% 3.85/1.16 fof(f1777,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Ack(sK11_skl,X0),queue(host(sK9_skl)))|~host(X0)=host(sK13_skl)|~sQ75_spl)),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f910,f1776])).
% 3.85/1.16 fof(f1814,plain,(
% 3.85/1.16 ~index(ldr,host(sK10_skl))=host(sK10_skl)|~index(status,host(sK10_skl))=norm|~sQ1_spl),
% 3.85/1.16 inference(resolution,[status(thm)],[f258,f251])).
% 3.85/1.16 fof(f1823,definition,(
% 3.85/1.16 sQ140_spl <=> (index(ldr,host(sK10_skl))=host(sK10_skl))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f1825,plain,(
% 3.85/1.16 ~index(ldr,host(sK10_skl))=host(sK10_skl)|sQ140_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f1823])).
% 3.85/1.16 fof(f1826,definition,(
% 3.85/1.16 sQ141_spl <=> (index(status,host(sK10_skl))=norm)),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f1828,plain,(
% 3.85/1.16 ~index(status,host(sK10_skl))=norm|sQ141_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f1826])).
% 3.85/1.16 fof(f1829,plain,(
% 3.85/1.16 ~sQ140_spl|~sQ141_spl|~sQ1_spl),
% 3.85/1.16 inference(split_clause,[status(thm)],[f1814,f1823,f1826,f257])).
% 3.85/1.16 fof(f1838,plain,(
% 3.85/1.16 ~norm=norm|sQ141_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f253,f1828])).
% 3.85/1.16 fof(f1839,plain,(
% 3.85/1.16 $false|sQ141_spl),
% 3.85/1.16 inference(trivial_equality_resolution,[status(thm)],[f1838])).
% 3.85/1.16 fof(f1840,plain,(
% 3.85/1.16 sQ141_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f1839])).
% 3.85/1.16 fof(f1841,plain,(
% 3.85/1.16 ~host(sK10_skl)=host(sK10_skl)|sQ140_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f252,f1825])).
% 3.85/1.16 fof(f1842,plain,(
% 3.85/1.16 $false|sQ140_spl),
% 3.85/1.16 inference(trivial_equality_resolution,[status(thm)],[f1841])).
% 3.85/1.16 fof(f1843,plain,(
% 3.85/1.16 sQ140_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f1842])).
% 3.85/1.16 fof(f1962,definition,(
% 3.85/1.16 sQ154_spl <=> (q_nil=cons(head(q_nil),q_nil))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f1963,plain,(
% 3.85/1.16 q_nil=cons(head(q_nil),q_nil)|~sQ154_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f1962])).
% 3.85/1.16 fof(f1966,plain,(
% 3.85/1.16 $false|~sQ154_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f1963,f133])).
% 3.85/1.16 fof(f1967,plain,(
% 3.85/1.16 ~sQ154_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f1966])).
% 3.85/1.16 fof(f2112,definition,(
% 3.85/1.16 sQ158_spl <=> (zero=s(nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2113,plain,(
% 3.85/1.16 zero=s(nbr_proc)|~sQ158_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2112])).
% 3.85/1.16 fof(f2115,definition,(
% 3.85/1.16 sQ159_spl <=> (leq(zero,nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2130,plain,(
% 3.85/1.16 ~leq(zero,nbr_proc)|~sQ158_spl),
% 3.85/1.16 inference(paramodulation,[status(thm)],[f2113,f191])).
% 3.85/1.16 fof(f2143,definition,(
% 3.85/1.16 sQ161_spl <=> (m_Down(sK12_skl)=last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2144,plain,(
% 3.85/1.16 m_Down(sK12_skl)=last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl)))|~sQ161_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2143])).
% 3.85/1.16 fof(f2150,definition,(
% 3.85/1.16 sQ163_spl <=> (m_Ack(sK11_skl,sK13_skl)=last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2151,plain,(
% 3.85/1.16 m_Ack(sK11_skl,sK13_skl)=last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl)))|~sQ163_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2150])).
% 3.85/1.16 fof(f2161,plain,(
% 3.85/1.16 m_Down(sK12_skl)=m_Ldr(sK4_skl)|~sQ161_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f129,f2144])).
% 3.85/1.16 fof(f2162,plain,(
% 3.85/1.16 $false|~sQ161_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2161,f90])).
% 3.85/1.16 fof(f2163,plain,(
% 3.85/1.16 ~sQ161_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f2162])).
% 3.85/1.16 fof(f2164,plain,(
% 3.85/1.16 m_Ack(sK11_skl,sK13_skl)=m_Ldr(sK4_skl)|~sQ163_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f129,f2151])).
% 3.85/1.16 fof(f2165,plain,(
% 3.85/1.16 $false|~sQ163_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2164,f86])).
% 3.85/1.16 fof(f2166,plain,(
% 3.85/1.16 ~sQ163_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f2165])).
% 3.85/1.16 fof(f2169,plain,(
% 3.85/1.16 $false|~sQ158_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2130,f1169])).
% 3.85/1.16 fof(f2170,plain,(
% 3.85/1.16 ~sQ158_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f2169])).
% 3.85/1.16 fof(f2250,definition,(
% 3.85/1.16 sQ166_spl <=> (leq(nbr_proc,nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2252,plain,(
% 3.85/1.16 ~leq(nbr_proc,nbr_proc)|sQ166_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2250])).
% 3.85/1.16 fof(f2434,plain,(
% 3.85/1.16 ![X0]: (leq(X0,nbr_proc)|leq(zero,X0))),
% 3.85/1.16 inference(resolution,[status(thm)],[f494,f1169])).
% 3.85/1.16 fof(f2638,definition,(
% 3.85/1.16 sQ189_spl <=> (s(zero)=s(nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2639,plain,(
% 3.85/1.16 s(zero)=s(nbr_proc)|~sQ189_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2638])).
% 3.85/1.16 fof(f2726,definition,(
% 3.85/1.16 sQ197_spl <=> (q_nil=snoc(q_nil,last(q_nil)))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2727,plain,(
% 3.85/1.16 q_nil=snoc(q_nil,last(q_nil))|~sQ197_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2726])).
% 3.85/1.16 fof(f2730,plain,(
% 3.85/1.16 q_nil=cons(last(q_nil),q_nil)|~sQ197_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f135,f2727])).
% 3.85/1.16 fof(f2731,plain,(
% 3.85/1.16 $false|~sQ197_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2730,f133])).
% 3.85/1.16 fof(f2732,plain,(
% 3.85/1.16 ~sQ197_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f2731])).
% 3.85/1.16 fof(f2954,definition,(
% 3.85/1.16 sQ207_spl <=> (leq(host(sK13_skl),host(sK13_skl)))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2956,plain,(
% 3.85/1.16 ~leq(host(sK13_skl),host(sK13_skl))|sQ207_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2954])).
% 3.85/1.16 fof(f2968,definition,(
% 3.85/1.16 sQ211_spl <=> (leq(index(pendack,host(sK9_skl)),host(sK13_skl)))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f2970,plain,(
% 3.85/1.16 ~leq(index(pendack,host(sK9_skl)),host(sK13_skl))|sQ211_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f2968])).
% 3.85/1.16 fof(f2990,plain,(
% 3.85/1.16 ~leq(host(sK13_skl),host(sK13_skl))|sQ211_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f910,f2970])).
% 3.85/1.16 fof(f2991,plain,(
% 3.85/1.16 $false|sQ211_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2990,f192])).
% 3.85/1.16 fof(f2992,plain,(
% 3.85/1.16 sQ211_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f2991])).
% 3.85/1.16 fof(f2993,plain,(
% 3.85/1.16 $false|sQ207_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2956,f192])).
% 3.85/1.16 fof(f2994,plain,(
% 3.85/1.16 sQ207_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f2993])).
% 3.85/1.16 fof(f3294,plain,(
% 3.85/1.16 ~leq(s(zero),nbr_proc)|~sQ189_spl),
% 3.85/1.16 inference(paramodulation,[status(thm)],[f2639,f191])).
% 3.85/1.16 fof(f3298,plain,(
% 3.85/1.16 $false|~sQ189_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f3294,f75])).
% 3.85/1.16 fof(f3299,plain,(
% 3.85/1.16 ~sQ189_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f3298])).
% 3.85/1.16 fof(f3810,definition,(
% 3.85/1.16 ![X0]: (sQ235_spl <=> (m_Down(sK12_skl)=X0))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f3811,plain,(
% 3.85/1.16 ![X0]: (m_Down(sK12_skl)=X0|~sQ235_spl)),
% 3.85/1.16 inference(component_clause,[status(thm)],[f3810])).
% 3.85/1.16 fof(f3828,plain,(
% 3.85/1.16 $false|~sQ235_spl),
% 3.85/1.16 inference(resolution,[status(thm)],[f3811,f92])).
% 3.85/1.16 fof(f3854,plain,(
% 3.85/1.16 ~sQ235_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f3828])).
% 3.85/1.16 fof(f3921,definition,(
% 3.85/1.16 ![X0]: (sQ247_spl <=> (m_Ack(sK11_skl,sK13_skl)=X0))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f3922,plain,(
% 3.85/1.16 ![X0]: (m_Ack(sK11_skl,sK13_skl)=X0|~sQ247_spl)),
% 3.85/1.16 inference(component_clause,[status(thm)],[f3921])).
% 3.85/1.16 fof(f3941,plain,(
% 3.85/1.16 $false|~sQ247_spl),
% 3.85/1.16 inference(resolution,[status(thm)],[f3922,f87])).
% 3.85/1.16 fof(f3967,plain,(
% 3.85/1.16 ~sQ247_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f3941])).
% 3.85/1.16 fof(f4008,definition,(
% 3.85/1.16 sQ252_spl <=> (leq(host(sK9_skl),nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f4010,plain,(
% 3.85/1.16 ~leq(host(sK9_skl),nbr_proc)|sQ252_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f4008])).
% 3.85/1.16 fof(f4013,plain,(
% 3.85/1.16 $false|sQ252_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f4010,f76])).
% 3.85/1.16 fof(f4014,plain,(
% 3.85/1.16 sQ252_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f4013])).
% 3.85/1.16 fof(f4058,definition,(
% 3.85/1.16 sQ254_spl <=> (leq(host(sK13_skl),nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f4060,plain,(
% 3.85/1.16 ~leq(host(sK13_skl),nbr_proc)|sQ254_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f4058])).
% 3.85/1.16 fof(f4069,definition,(
% 3.85/1.16 sQ257_spl <=> (leq(index(pendack,host(sK9_skl)),nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f4071,plain,(
% 3.85/1.16 ~leq(index(pendack,host(sK9_skl)),nbr_proc)|sQ257_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f4069])).
% 3.85/1.16 fof(f4087,plain,(
% 3.85/1.16 ~leq(host(sK13_skl),nbr_proc)|sQ257_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f910,f4071])).
% 3.85/1.16 fof(f4088,plain,(
% 3.85/1.16 $false|sQ257_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f4087,f76])).
% 3.85/1.16 fof(f4089,plain,(
% 3.85/1.16 sQ257_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f4088])).
% 3.85/1.16 fof(f4090,plain,(
% 3.85/1.16 $false|sQ166_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f2252,f192])).
% 3.85/1.16 fof(f4091,plain,(
% 3.85/1.16 sQ166_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f4090])).
% 3.85/1.16 fof(f4092,plain,(
% 3.85/1.16 $false|sQ254_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f4060,f76])).
% 3.85/1.16 fof(f4093,plain,(
% 3.85/1.16 sQ254_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f4092])).
% 3.85/1.16 fof(f4272,plain,(
% 3.85/1.16 ![X0]: (~elem(m_Down(X0),queue(host(sK9_skl)))|~host(X0)=nbr_proc|~sQ85_spl|~sQ74_spl)),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f1040,f1015])).
% 3.85/1.16 fof(f4273,plain,(
% 3.85/1.16 ~host(sK12_skl)=nbr_proc|~sQ85_spl|~sQ74_spl|~sQ51_spl),
% 3.85/1.16 inference(resolution,[status(thm)],[f4272,f814])).
% 3.85/1.16 fof(f4274,plain,(
% 3.85/1.16 ~nbr_proc=nbr_proc|~sQ85_spl|~sQ74_spl|~sQ51_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f1040,f4273])).
% 3.85/1.16 fof(f4275,plain,(
% 3.85/1.16 $false|~sQ85_spl|~sQ74_spl|~sQ51_spl),
% 3.85/1.16 inference(trivial_equality_resolution,[status(thm)],[f4274])).
% 3.85/1.16 fof(f4276,plain,(
% 3.85/1.16 ~sQ85_spl|~sQ74_spl|~sQ51_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f4275])).
% 3.85/1.16 fof(f6223,definition,(
% 3.85/1.16 sQ324_spl <=> (leq(host(sK13_skl),index(pendack,host(sK9_skl))))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f6225,plain,(
% 3.85/1.16 ~leq(host(sK13_skl),index(pendack,host(sK9_skl)))|sQ324_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f6223])).
% 3.85/1.16 fof(f6240,plain,(
% 3.85/1.16 ~leq(host(sK13_skl),host(sK13_skl))|sQ324_spl),
% 3.85/1.16 inference(forward_demodulation,[status(thm)],[f910,f6225])).
% 3.85/1.16 fof(f6241,plain,(
% 3.85/1.16 $false|sQ324_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f6240,f192])).
% 3.85/1.16 fof(f6242,plain,(
% 3.85/1.16 sQ324_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f6241])).
% 3.85/1.16 fof(f6967,plain,(
% 3.85/1.16 leq(zero,nbr_proc)|leq(zero,nbr_proc)),
% 3.85/1.16 inference(resolution,[status(thm)],[f2434,f1335])).
% 3.85/1.16 fof(f6992,plain,(
% 3.85/1.16 sQ159_spl),
% 3.85/1.16 inference(split_clause,[status(thm)],[f6967,f2115])).
% 3.85/1.16 fof(f7073,definition,(
% 3.85/1.16 sQ354_spl <=> (leq(nbr_proc,s(nbr_proc)))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f7075,plain,(
% 3.85/1.16 ~leq(nbr_proc,s(nbr_proc))|sQ354_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f7073])).
% 3.85/1.16 fof(f7083,plain,(
% 3.85/1.16 $false|sQ354_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f7075,f318])).
% 3.85/1.16 fof(f7084,plain,(
% 3.85/1.16 sQ354_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f7083])).
% 3.85/1.16 fof(f7440,definition,(
% 3.85/1.16 sQ391_spl <=> (leq(host(sK4_skl),nbr_proc))),
% 3.85/1.16 introduced(definition,[new_symbols(definition,[sQ391_spl])],[split_symbol_definition])).
% 3.85/1.16 fof(f7442,plain,(
% 3.85/1.16 ~leq(host(sK4_skl),nbr_proc)|sQ391_spl),
% 3.85/1.16 inference(component_clause,[status(thm)],[f7440])).
% 3.85/1.16 fof(f7452,plain,(
% 3.85/1.16 $false|sQ391_spl),
% 3.85/1.16 inference(forward_subsumption_resolution,[status(thm)],[f7442,f76])).
% 3.85/1.16 fof(f7453,plain,(
% 3.85/1.16 sQ391_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f7452])).
% 3.85/1.16 fof(f7749,plain,(
% 3.85/1.16 ~host(sK13_skl)=host(sK13_skl)|~sQ75_spl|~sQ66_spl),
% 3.85/1.16 inference(resolution,[status(thm)],[f1777,f904])).
% 3.85/1.16 fof(f7750,plain,(
% 3.85/1.16 $false|~sQ75_spl|~sQ66_spl),
% 3.85/1.16 inference(trivial_equality_resolution,[status(thm)],[f7749])).
% 3.85/1.16 fof(f7751,plain,(
% 3.85/1.16 ~sQ75_spl|~sQ66_spl),
% 3.85/1.16 inference(contradiction_clause,[status(thm)],[f7750])).
% 3.85/1.16 fof(f7752,plain,(
% 3.85/1.16 $false),
% 3.85/1.16 inference(sat_refutation,[status(thm)],[f260,f316,f588,f816,f818,f906,f908,f962,f1012,f1042,f1044,f1829,f1840,f1843,f1967,f2163,f2166,f2170,f2732,f2992,f2994,f3299,f3854,f3967,f4014,f4089,f4091,f4093,f4276,f6242,f6992,f7084,f7453,f7751])).
% 3.85/1.17 % SZS output end CNFRefutation for theBenchmark.p
% 3.85/1.19 % Elapsed time: 0.821748 seconds
% 3.85/1.19 % CPU time: 6.222157 seconds
% 3.85/1.19 % Total memory used: 153.420 MB
% 3.85/1.19 % Net memory used: 146.083 MB
%------------------------------------------------------------------------------