%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV479+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:48:01 PM UTC 2026
% Result : Theorem 0.12s 16.11s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 48
% Syntax : Number of formulae : 220 ( 51 unt; 35 def)
% Number of atoms : 1148 ( 411 equ)
% Maximal formula atoms : 126 ( 5 avg)
% Number of connectives : 1505 ( 577 ~; 507 |; 323 &)
% ( 39 <=>; 59 =>; 0 <=; 0 <~>)
% Maximal formula depth : 44 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 41 ( 39 usr; 36 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 22 con; 0-4 aty)
% Number of variables : 388 ( 363 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [P] : leq(s(zero),host(P)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [P] : leq(host(P),nbr_proc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X,Y] : m_Down(X) != m_Halt(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [X,Q] : q_nil != cons(X,Q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [Y,Q] : q_nil != snoc(Q,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X] :
( pidElem(X)
<=> ? [Y] :
( X = m_Down(Y)
| X = m_Halt(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [X] : ~ leq(s(X),X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [X,Y] :
( ( leq(Y,X)
& leq(X,Y) )
<=> X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X,Y,Z] :
( ( leq(Y,Z)
& leq(X,Y) )
=> leq(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [X,Y] :
( leq(X,Y)
<=> leq(s(X),s(Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [X,Y] :
( leq(X,s(Y))
<=> ( leq(X,Y)
| X = s(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,conjecture,
! [V,W,X,Y] :
( ( queue(host(X)) = cons(m_Down(Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& host(Pid30) = s(host(Pid0))
& elem(m_Down(Pid30),queue(host(Pid0)))
& elem(m_Down(Pid20),queue(host(Pid0)))
& leq(nbr_proc,s(host(Pid0)))
& setIn(Pid0,alive)
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& index(status,host(Z)) = elec_2
& host(Pid30) = host(Pid0)
& elem(m_Down(Pid20),queue(host(Pid0)))
& leq(host(Z),host(Pid0))
& setIn(Z,alive)
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ elem(m_Ack(Z,Pid30),queue(host(Z))) )
& ! [Z,Pid20,Pid0] :
( ( host(index(elid,host(Pid0))) = host(Pid20)
& index(status,host(Pid0)) = wait
& host(Pid20) = host(Z)
& elem(m_Down(Z),queue(host(Pid0)))
& setIn(Pid0,alive)
& host(Pid0) != host(Pid20) )
=> ~ ( index(ldr,host(Pid20)) = host(Pid20)
& index(status,host(Pid20)) = norm
& setIn(Pid20,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid20)
& index(status,host(Pid0)) = norm
& host(Pid20) = host(Z)
& elem(m_Down(Z),queue(host(Pid0)))
& setIn(Pid0,alive)
& host(Pid0) != host(Pid20) )
=> ~ ( index(ldr,host(Pid20)) = host(Pid20)
& index(status,host(Pid20)) = norm
& setIn(Pid20,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid0) = host(Pid20)
& host(Pid30) = host(Z)
& setIn(Pid20,alive)
& setIn(Z,alive)
& host(Pid20) != host(Z) )
=> ~ ( setIn(host(Pid30),index(down,host(Pid20)))
& elem(m_Down(Pid0),queue(host(Z))) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid0) = host(Pid20)
& host(Pid30) = host(Z)
& setIn(Pid20,alive)
& setIn(Z,alive)
& host(Pid20) != host(Z) )
=> ~ ( elem(m_Down(Pid30),queue(host(Pid20)))
& elem(m_Down(Pid0),queue(host(Z))) ) )
& ! [Z,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive)
& ~ leq(host(Pid20),host(Pid0)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> Pid0 = Z )
& ! [Z,Pid20,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& host(Pid20) = host(Pid0)
& setIn(Pid0,alive) )
=> ~ ( elem(m_Down(Pid20),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& host(Pid0) = host(Pid20)
& elem(m_Down(Pid20),queue(host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& setIn(Pid0,alive) )
=> ~ ( setIn(host(Pid0),index(down,host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& setIn(host(Pid0),index(down,host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z] :
( ( setIn(Z,alive)
& ( index(status,host(Z)) = elec_2
| index(status,host(Z)) = elec_1 ) )
=> index(elid,host(Z)) = Z )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid0] :
( elem(m_Down(Pid0),queue(host(Z)))
=> host(Pid0) != host(Z) )
& ! [Z,Pid0] :
( elem(m_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( leq(host(X),host(Y))
=> ( ( host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2 )
=> ( leq(nbr_proc,index(pendack,host(X)))
=> ! [Z] :
( setIn(host(Z),index(acks,host(X)))
=> ! [V0] :
( host(X) = host(V0)
=> ! [W0,X0,Y0] :
( host(Z) != host(Y0)
=> ( host(X) != host(Y0)
=> ( ( index(status,host(Y0)) = elec_1
& host(W0) = s(host(Y0))
& elem(m_Down(X0),queue(host(Y0)))
& elem(m_Down(W0),queue(host(Y0)))
& leq(nbr_proc,s(host(Y0)))
& setIn(Y0,alive)
& ! [V1] :
( ( leq(s(zero),V1)
& ~ leq(host(Y0),V1) )
=> ( V1 = host(X0)
| setIn(V1,index(down,host(Y0))) ) ) )
=> ~ ( host(X) = host(V0)
& setIn(V0,alive) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,negated_conjecture,
~ ! [V,W,X,Y] :
( ( queue(host(X)) = cons(m_Down(Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& host(Pid30) = s(host(Pid0))
& elem(m_Down(Pid30),queue(host(Pid0)))
& elem(m_Down(Pid20),queue(host(Pid0)))
& leq(nbr_proc,s(host(Pid0)))
& setIn(Pid0,alive)
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& index(status,host(Z)) = elec_2
& host(Pid30) = host(Pid0)
& elem(m_Down(Pid20),queue(host(Pid0)))
& leq(host(Z),host(Pid0))
& setIn(Z,alive)
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ elem(m_Ack(Z,Pid30),queue(host(Z))) )
& ! [Z,Pid20,Pid0] :
( ( host(index(elid,host(Pid0))) = host(Pid20)
& index(status,host(Pid0)) = wait
& host(Pid20) = host(Z)
& elem(m_Down(Z),queue(host(Pid0)))
& setIn(Pid0,alive)
& host(Pid0) != host(Pid20) )
=> ~ ( index(ldr,host(Pid20)) = host(Pid20)
& index(status,host(Pid20)) = norm
& setIn(Pid20,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid20)
& index(status,host(Pid0)) = norm
& host(Pid20) = host(Z)
& elem(m_Down(Z),queue(host(Pid0)))
& setIn(Pid0,alive)
& host(Pid0) != host(Pid20) )
=> ~ ( index(ldr,host(Pid20)) = host(Pid20)
& index(status,host(Pid20)) = norm
& setIn(Pid20,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid0) = host(Pid20)
& host(Pid30) = host(Z)
& setIn(Pid20,alive)
& setIn(Z,alive)
& host(Pid20) != host(Z) )
=> ~ ( setIn(host(Pid30),index(down,host(Pid20)))
& elem(m_Down(Pid0),queue(host(Z))) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid0) = host(Pid20)
& host(Pid30) = host(Z)
& setIn(Pid20,alive)
& setIn(Z,alive)
& host(Pid20) != host(Z) )
=> ~ ( elem(m_Down(Pid30),queue(host(Pid20)))
& elem(m_Down(Pid0),queue(host(Z))) ) )
& ! [Z,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive)
& ~ leq(host(Pid20),host(Pid0)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> Pid0 = Z )
& ! [Z,Pid20,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& host(Pid20) = host(Pid0)
& setIn(Pid0,alive) )
=> ~ ( elem(m_Down(Pid20),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& host(Pid0) = host(Pid20)
& elem(m_Down(Pid20),queue(host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& setIn(Pid0,alive) )
=> ~ ( setIn(host(Pid0),index(down,host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& setIn(host(Pid0),index(down,host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z] :
( ( setIn(Z,alive)
& ( index(status,host(Z)) = elec_2
| index(status,host(Z)) = elec_1 ) )
=> index(elid,host(Z)) = Z )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid0] :
( elem(m_Down(Pid0),queue(host(Z)))
=> host(Pid0) != host(Z) )
& ! [Z,Pid0] :
( elem(m_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( leq(host(X),host(Y))
=> ( ( host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2 )
=> ( leq(nbr_proc,index(pendack,host(X)))
=> ! [Z] :
( setIn(host(Z),index(acks,host(X)))
=> ! [V0] :
( host(X) = host(V0)
=> ! [W0,X0,Y0] :
( host(Z) != host(Y0)
=> ( host(X) != host(Y0)
=> ( ( index(status,host(Y0)) = elec_1
& host(W0) = s(host(Y0))
& elem(m_Down(X0),queue(host(Y0)))
& elem(m_Down(W0),queue(host(Y0)))
& leq(nbr_proc,s(host(Y0)))
& setIn(Y0,alive)
& ! [V1] :
( ( leq(s(zero),V1)
& ~ leq(host(Y0),V1) )
=> ( V1 = host(X0)
| setIn(V1,index(down,host(Y0))) ) ) )
=> ~ ( host(X) = host(V0)
& setIn(V0,alive) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f67]) ).
fof(f74,plain,
! [X0] : leq(s(zero),host(X0)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f76,plain,
! [X0] : leq(host(X0),nbr_proc),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f89,plain,
! [X0,X1] : m_Down(X0) != m_Halt(X1),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f133,plain,
! [X0,X1] : q_nil != cons(X0,X1),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f134,plain,
! [X0,X1] : q_nil != snoc(X0,X1),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f148,plain,
! [X] :
( ( ! [Y] :
( X != m_Down(Y)
& X != m_Halt(Y) )
| pidElem(X) )
& ( ? [Y] :
( X = m_Down(Y)
| X = m_Halt(Y) )
| ~ pidElem(X) ) ),
inference(NNF_transformation,[status(thm)],[f49]) ).
fof(f149,plain,
( ! [X] :
( ( ! [Y] : X != m_Down(Y)
& ! [Y] : X != m_Halt(Y) )
| pidElem(X) )
& ! [X] :
( ? [Y] : X = m_Down(Y)
| ? [Y] : X = m_Halt(Y)
| ~ pidElem(X) ) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f150,plain,
( ! [X] :
( ( ! [Y] : X != m_Down(Y)
& ! [Y] : X != m_Halt(Y) )
| pidElem(X) )
& ! [X] :
( X = m_Down(sK1_skl(X))
| X = m_Halt(sK0_skl(X))
| ~ pidElem(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl(X)),skolemize(Y,sK1_skl(X))],[f149]) ).
fof(f153,plain,
! [X0,X1] :
( X0 != m_Down(X1)
| pidElem(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f191,plain,
! [X0] : ~ leq(s(X0),X0),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f192,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f194,plain,
! [X,Y] :
( ( X != Y
| ( leq(Y,X)
& leq(X,Y) ) )
& ( X = Y
| ~ leq(Y,X)
| ~ leq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f62]) ).
fof(f195,plain,
( ! [X,Y] :
( X != Y
| ( leq(Y,X)
& leq(X,Y) ) )
& ! [X,Y] :
( X = Y
| ~ leq(Y,X)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f194]) ).
fof(f196,plain,
! [X0,X1] :
( X0 = X1
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f199,plain,
! [X,Y,Z] :
( leq(X,Z)
| ~ leq(Y,Z)
| ~ leq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f200,plain,
! [X,Z] :
( leq(X,Z)
| ! [Y] :
( ~ leq(Y,Z)
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f201,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [X,Y] :
( ( ~ leq(s(X),s(Y))
| leq(X,Y) )
& ( leq(s(X),s(Y))
| ~ leq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f64]) ).
fof(f203,plain,
( ! [X,Y] :
( ~ leq(s(X),s(Y))
| leq(X,Y) )
& ! [X,Y] :
( leq(s(X),s(Y))
| ~ leq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f202]) ).
fof(f204,plain,
! [X0,X1] :
( leq(s(X0),s(X1))
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f205,plain,
! [X0,X1] :
( ~ leq(s(X0),s(X1))
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f206,plain,
! [X,Y] :
( ( ( ~ leq(X,Y)
& X != s(Y) )
| leq(X,s(Y)) )
& ( leq(X,Y)
| X = s(Y)
| ~ leq(X,s(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f207,plain,
( ! [X,Y] :
( ( ~ leq(X,Y)
& X != s(Y) )
| leq(X,s(Y)) )
& ! [X,Y] :
( leq(X,Y)
| X = s(Y)
| ~ leq(X,s(Y)) ) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f208,plain,
! [X0,X1] :
( leq(X0,X1)
| X0 = s(X1)
| ~ leq(X0,s(X1)) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f210,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| leq(X0,s(X1)) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f212,plain,
? [V,W,X,Y] :
( ? [Z] :
( ? [V0] :
( ? [W0,X0,Y0] :
( host(X) = host(V0)
& setIn(V0,alive)
& index(status,host(Y0)) = elec_1
& host(W0) = s(host(Y0))
& elem(m_Down(X0),queue(host(Y0)))
& elem(m_Down(W0),queue(host(Y0)))
& leq(nbr_proc,s(host(Y0)))
& setIn(Y0,alive)
& ! [V1] :
( V1 = host(X0)
| setIn(V1,index(down,host(Y0)))
| ~ leq(s(zero),V1)
| leq(host(Y0),V1) )
& host(X) != host(Y0)
& host(Z) != host(Y0) )
& host(X) = host(V0) )
& setIn(host(Z),index(acks,host(X))) )
& leq(nbr_proc,index(pendack,host(X)))
& host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2
& leq(host(X),host(Y))
& setIn(X,alive)
& queue(host(X)) = cons(m_Down(Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_1
| host(Pid30) != s(host(Pid0))
| ~ elem(m_Down(Pid30),queue(host(Pid0)))
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ leq(nbr_proc,s(host(Pid0)))
| ~ setIn(Pid0,alive)
| ? [V0] :
( V0 != host(Pid20)
& ~ setIn(V0,index(down,host(Pid0)))
& leq(s(zero),V0)
& ~ leq(host(Pid0),V0) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ elem(m_Ack(Z,Pid30),queue(host(Z)))
| index(status,host(Pid0)) != elec_1
| index(status,host(Z)) != elec_2
| host(Pid30) != host(Pid0)
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ leq(host(Z),host(Pid0))
| ~ setIn(Z,alive)
| ? [V0] :
( V0 != host(Pid20)
& ~ setIn(V0,index(down,host(Pid0)))
& leq(s(zero),V0)
& ~ leq(host(Pid0),V0) ) )
& ! [Z,Pid20,Pid0] :
( index(ldr,host(Pid20)) != host(Pid20)
| index(status,host(Pid20)) != norm
| ~ setIn(Pid20,alive)
| host(index(elid,host(Pid0))) != host(Pid20)
| index(status,host(Pid0)) != wait
| host(Pid20) != host(Z)
| ~ elem(m_Down(Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| host(Pid0) = host(Pid20) )
& ! [Z,Pid20,Pid0] :
( index(ldr,host(Pid20)) != host(Pid20)
| index(status,host(Pid20)) != norm
| ~ setIn(Pid20,alive)
| index(ldr,host(Pid0)) != host(Pid20)
| index(status,host(Pid0)) != norm
| host(Pid20) != host(Z)
| ~ elem(m_Down(Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| host(Pid0) = host(Pid20) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ setIn(host(Pid30),index(down,host(Pid20)))
| ~ elem(m_Down(Pid0),queue(host(Z)))
| host(Pid0) != host(Pid20)
| host(Pid30) != host(Z)
| ~ setIn(Pid20,alive)
| ~ setIn(Z,alive)
| host(Pid20) = host(Z) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ elem(m_Down(Pid30),queue(host(Pid20)))
| ~ elem(m_Down(Pid0),queue(host(Z)))
| host(Pid0) != host(Pid20)
| host(Pid30) != host(Z)
| ~ setIn(Pid20,alive)
| ~ setIn(Z,alive)
| host(Pid20) = host(Z) )
& ! [Z,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| host(Pid20) != host(Z)
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| leq(host(Pid20),host(Pid0)) )
& ! [Z,Pid0] :
( Pid0 = Z
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Z,Pid20,Pid0] :
( ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Z,alive)
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| host(Pid20) != host(Pid0)
| ~ setIn(Pid0,alive) )
& ! [Z,Pid20,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| host(Pid0) != host(Pid20)
| ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Z,Pid0] :
( ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Z,alive)
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Z] :
( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid0] :
( host(Pid0) != host(Z)
| ~ elem(m_Down(Pid0),queue(host(Z))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ldr(Pid0),queue(host(Z))) ) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f213,plain,
? [X,Y] :
( ? [Z] :
( ? [V0] :
( ? [Y0] :
( host(X) = host(V0)
& setIn(V0,alive)
& index(status,host(Y0)) = elec_1
& ? [W0] :
( host(W0) = s(host(Y0))
& ? [X0] :
( elem(m_Down(X0),queue(host(Y0)))
& elem(m_Down(W0),queue(host(Y0)))
& leq(nbr_proc,s(host(Y0)))
& setIn(Y0,alive)
& ! [V1] :
( V1 = host(X0)
| setIn(V1,index(down,host(Y0)))
| ~ leq(s(zero),V1)
| leq(host(Y0),V1) ) ) )
& host(X) != host(Y0)
& host(Z) != host(Y0) )
& host(X) = host(V0) )
& setIn(host(Z),index(acks,host(X))) )
& leq(nbr_proc,index(pendack,host(X)))
& host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2
& leq(host(X),host(Y))
& setIn(X,alive)
& ? [V] : queue(host(X)) = cons(m_Down(Y),V)
& ( ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive) )
| ! [Pid0] :
( index(status,host(Pid0)) != elec_1
| ! [Pid30] :
( host(Pid30) != s(host(Pid0))
| ~ elem(m_Down(Pid30),queue(host(Pid0)))
| ! [Pid20] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ leq(nbr_proc,s(host(Pid0)))
| ~ setIn(Pid0,alive)
| ? [V0] :
( V0 != host(Pid20)
& ~ setIn(V0,index(down,host(Pid0)))
& leq(s(zero),V0)
& ~ leq(host(Pid0),V0) ) ) ) ) )
& ! [Z,Pid30] :
( ~ elem(m_Ack(Z,Pid30),queue(host(Z)))
| ! [Pid0] :
( index(status,host(Pid0)) != elec_1
| index(status,host(Z)) != elec_2
| host(Pid30) != host(Pid0)
| ! [Pid20] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ leq(host(Z),host(Pid0))
| ~ setIn(Z,alive)
| ? [V0] :
( V0 != host(Pid20)
& ~ setIn(V0,index(down,host(Pid0)))
& leq(s(zero),V0)
& ~ leq(host(Pid0),V0) ) ) ) )
& ! [Pid20] :
( index(ldr,host(Pid20)) != host(Pid20)
| index(status,host(Pid20)) != norm
| ~ setIn(Pid20,alive)
| ! [Pid0] :
( host(index(elid,host(Pid0))) != host(Pid20)
| index(status,host(Pid0)) != wait
| ! [Z] :
( host(Pid20) != host(Z)
| ~ elem(m_Down(Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| host(Pid0) = host(Pid20) ) ) )
& ! [Pid20] :
( index(ldr,host(Pid20)) != host(Pid20)
| index(status,host(Pid20)) != norm
| ~ setIn(Pid20,alive)
| ! [Pid0] :
( index(ldr,host(Pid0)) != host(Pid20)
| index(status,host(Pid0)) != norm
| ! [Z] :
( host(Pid20) != host(Z)
| ~ elem(m_Down(Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| host(Pid0) = host(Pid20) ) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ setIn(host(Pid30),index(down,host(Pid20)))
| ~ elem(m_Down(Pid0),queue(host(Z)))
| host(Pid0) != host(Pid20)
| host(Pid30) != host(Z)
| ~ setIn(Pid20,alive)
| ~ setIn(Z,alive)
| host(Pid20) = host(Z) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ elem(m_Down(Pid30),queue(host(Pid20)))
| ~ elem(m_Down(Pid0),queue(host(Z)))
| host(Pid0) != host(Pid20)
| host(Pid30) != host(Z)
| ~ setIn(Pid20,alive)
| ~ setIn(Z,alive)
| host(Pid20) = host(Z) )
& ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| ! [Pid20] :
( host(Pid20) != host(Z)
| ! [Pid0] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| leq(host(Pid20),host(Pid0)) ) ) )
& ! [Z,Pid0] :
( Pid0 = Z
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Pid20] :
( ! [Z] :
( ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Z,alive) )
| ! [Pid0] :
( index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| host(Pid20) != host(Pid0)
| ~ setIn(Pid0,alive) ) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| ! [Pid20] :
( host(Pid0) != host(Pid20)
| ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Pid0] :
( ! [Z] :
( ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Z,alive) )
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Z] :
( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid0] :
( host(Pid0) != host(Z)
| ~ elem(m_Down(Pid0),queue(host(Z))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ldr(Pid0),queue(host(Z))) ) ),
inference(miniscoping,[status(thm)],[f212]) ).
fof(f214,plain,
( host(sK4_skl) = host(sK10_skl)
& setIn(sK10_skl,alive)
& index(status,host(sK11_skl)) = elec_1
& host(sK12_skl) = s(host(sK11_skl))
& elem(m_Down(sK13_skl),queue(host(sK11_skl)))
& elem(m_Down(sK12_skl),queue(host(sK11_skl)))
& leq(nbr_proc,s(host(sK11_skl)))
& setIn(sK11_skl,alive)
& ! [V1] :
( V1 = host(sK13_skl)
| setIn(V1,index(down,host(sK11_skl)))
| ~ leq(s(zero),V1)
| leq(host(sK11_skl),V1) )
& host(sK4_skl) != host(sK11_skl)
& host(sK9_skl) != host(sK11_skl)
& host(sK4_skl) = host(sK10_skl)
& setIn(host(sK9_skl),index(acks,host(sK4_skl)))
& leq(nbr_proc,index(pendack,host(sK4_skl)))
& host(sK5_skl) = index(pendack,host(sK4_skl))
& index(status,host(sK4_skl)) = elec_2
& leq(host(sK4_skl),host(sK5_skl))
& setIn(sK4_skl,alive)
& queue(host(sK4_skl)) = cons(m_Down(sK5_skl),sK8_skl)
& ( ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive) )
| ! [Pid0] :
( index(status,host(Pid0)) != elec_1
| ! [Pid30] :
( host(Pid30) != s(host(Pid0))
| ~ elem(m_Down(Pid30),queue(host(Pid0)))
| ! [Pid20] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ leq(nbr_proc,s(host(Pid0)))
| ~ setIn(Pid0,alive)
| ( sK7_skl(Pid20,Pid30,Pid0) != host(Pid20)
& ~ setIn(sK7_skl(Pid20,Pid30,Pid0),index(down,host(Pid0)))
& leq(s(zero),sK7_skl(Pid20,Pid30,Pid0))
& ~ leq(host(Pid0),sK7_skl(Pid20,Pid30,Pid0)) ) ) ) ) )
& ! [Z,Pid30] :
( ~ elem(m_Ack(Z,Pid30),queue(host(Z)))
| ! [Pid0] :
( index(status,host(Pid0)) != elec_1
| index(status,host(Z)) != elec_2
| host(Pid30) != host(Pid0)
| ! [Pid20] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ leq(host(Z),host(Pid0))
| ~ setIn(Z,alive)
| ( sK6_skl(Pid20,Pid0,Pid30,Z) != host(Pid20)
& ~ setIn(sK6_skl(Pid20,Pid0,Pid30,Z),index(down,host(Pid0)))
& leq(s(zero),sK6_skl(Pid20,Pid0,Pid30,Z))
& ~ leq(host(Pid0),sK6_skl(Pid20,Pid0,Pid30,Z)) ) ) ) )
& ! [Pid20] :
( index(ldr,host(Pid20)) != host(Pid20)
| index(status,host(Pid20)) != norm
| ~ setIn(Pid20,alive)
| ! [Pid0] :
( host(index(elid,host(Pid0))) != host(Pid20)
| index(status,host(Pid0)) != wait
| ! [Z] :
( host(Pid20) != host(Z)
| ~ elem(m_Down(Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| host(Pid0) = host(Pid20) ) ) )
& ! [Pid20] :
( index(ldr,host(Pid20)) != host(Pid20)
| index(status,host(Pid20)) != norm
| ~ setIn(Pid20,alive)
| ! [Pid0] :
( index(ldr,host(Pid0)) != host(Pid20)
| index(status,host(Pid0)) != norm
| ! [Z] :
( host(Pid20) != host(Z)
| ~ elem(m_Down(Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| host(Pid0) = host(Pid20) ) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ setIn(host(Pid30),index(down,host(Pid20)))
| ~ elem(m_Down(Pid0),queue(host(Z)))
| host(Pid0) != host(Pid20)
| host(Pid30) != host(Z)
| ~ setIn(Pid20,alive)
| ~ setIn(Z,alive)
| host(Pid20) = host(Z) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ elem(m_Down(Pid30),queue(host(Pid20)))
| ~ elem(m_Down(Pid0),queue(host(Z)))
| host(Pid0) != host(Pid20)
| host(Pid30) != host(Z)
| ~ setIn(Pid20,alive)
| ~ setIn(Z,alive)
| host(Pid20) = host(Z) )
& ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| ! [Pid20] :
( host(Pid20) != host(Z)
| ! [Pid0] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| leq(host(Pid20),host(Pid0)) ) ) )
& ! [Z,Pid0] :
( Pid0 = Z
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Pid20] :
( ! [Z] :
( ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Z,alive) )
| ! [Pid0] :
( index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| host(Pid20) != host(Pid0)
| ~ setIn(Pid0,alive) ) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| ! [Pid20] :
( host(Pid0) != host(Pid20)
| ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Pid0] :
( ! [Z] :
( ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Z,alive) )
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Z] :
( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid0] :
( host(Pid0) != host(Z)
| ~ elem(m_Down(Pid0),queue(host(Z))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ldr(Pid0),queue(host(Z))) ) ),
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(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(V0,sK6_skl(Pid20,Pid0,Pid30,Z)),skolemize(V0,sK7_skl(Pid20,Pid30,Pid0)),skolemize(V,sK8_skl),skolemize(Z,sK9_skl),skolemize(V0,sK10_skl),skolemize(Y0,sK11_skl),skolemize(W0,sK12_skl),skolemize(X0,sK13_skl)],[f213]) ).
fof(f217,plain,
! [X0,X1] :
( ~ setIn(X0,alive)
| ~ setIn(X1,alive)
| host(X0) != host(X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f220,plain,
! [X0,X1] :
( leq(index(pendack,host(X1)),host(X0))
| index(status,host(X1)) != elec_2
| ~ setIn(host(X1),index(down,host(X0)))
| ~ setIn(X1,alive)
| ~ setIn(X0,alive) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f222,plain,
! [X0,X1,X2] :
( leq(index(pendack,host(X1)),host(X0))
| index(status,host(X1)) != elec_2
| host(X1) != host(X2)
| ~ elem(m_Down(X2),queue(host(X0)))
| ~ setIn(X1,alive)
| ~ setIn(X0,alive) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f239,plain,
setIn(sK4_skl,alive),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f240,plain,
leq(host(sK4_skl),host(sK5_skl)),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f241,plain,
index(status,host(sK4_skl)) = elec_2,
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f242,plain,
host(sK5_skl) = index(pendack,host(sK4_skl)),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f243,plain,
leq(nbr_proc,index(pendack,host(sK4_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f247,plain,
host(sK4_skl) != host(sK11_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f248,plain,
! [X0] :
( X0 = host(sK13_skl)
| setIn(X0,index(down,host(sK11_skl)))
| ~ leq(s(zero),X0)
| leq(host(sK11_skl),X0) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f249,plain,
setIn(sK11_skl,alive),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f250,plain,
leq(nbr_proc,s(host(sK11_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f251,plain,
elem(m_Down(sK12_skl),queue(host(sK11_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f252,plain,
elem(m_Down(sK13_skl),queue(host(sK11_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f253,plain,
host(sK12_skl) = s(host(sK11_skl)),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f279,plain,
! [X0] : pidElem(m_Down(X0)),
inference(destructive_equality_resolution,[status(thm)],[f153]) ).
fof(f306,plain,
! [X0] :
( ~ setIn(X0,alive)
| host(X0) != host(sK11_skl)
| X0 = sK11_skl ),
inference(resolution,[status(thm)],[f217,f249]) ).
fof(f321,plain,
leq(nbr_proc,host(sK12_skl)),
inference(backward_demodulation,[status(thm)],[f253,f250]) ).
fof(f352,plain,
( host(sK12_skl) = nbr_proc
| ~ leq(host(sK12_skl),nbr_proc) ),
inference(resolution,[status(thm)],[f196,f321]) ).
fof(f353,plain,
( host(sK5_skl) = host(sK4_skl)
| ~ leq(host(sK5_skl),host(sK4_skl)) ),
inference(resolution,[status(thm)],[f196,f240]) ).
fof(f360,definition,
( sQ13_spl
<=> leq(host(sK12_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f362,plain,
( sQ13_spl
| ~ leq(host(sK12_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f360]) ).
fof(f363,definition,
( sQ14_spl
<=> host(sK12_skl) = nbr_proc ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f364,plain,
( ~ sQ14_spl
| host(sK12_skl) = nbr_proc ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f366,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f352,f360,f363]) ).
fof(f367,definition,
( sQ15_spl
<=> leq(host(sK5_skl),host(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f369,plain,
( sQ15_spl
| ~ leq(host(sK5_skl),host(sK4_skl)) ),
inference(component_clause,[status(thm)],[f367]) ).
fof(f370,definition,
( sQ16_spl
<=> host(sK5_skl) = host(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f371,plain,
( ~ sQ16_spl
| host(sK5_skl) = host(sK4_skl) ),
inference(component_clause,[status(thm)],[f370]) ).
fof(f373,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f353,f367,f370]) ).
fof(f381,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f362,f76]) ).
fof(f382,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f381]) ).
fof(f389,plain,
( ~ sQ14_spl
| nbr_proc = s(host(sK11_skl)) ),
inference(backward_demodulation,[status(thm)],[f364,f253]) ).
fof(f621,definition,
( sQ49_spl
<=> index(status,host(sK4_skl)) = elec_2 ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ49_spl
| index(status,host(sK4_skl)) != elec_2 ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f773,plain,
( ~ sQ14_spl
| ~ leq(nbr_proc,host(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f389,f191]) ).
fof(f775,plain,
! [X0,X1] :
( leq(X0,nbr_proc)
| ~ leq(X0,host(X1)) ),
inference(resolution,[status(thm)],[f201,f76]) ).
fof(f784,plain,
! [X0,X1] :
( ~ leq(X1,X0)
| ~ leq(s(X0),X1) ),
inference(resolution,[status(thm)],[f201,f191]) ).
fof(f791,plain,
! [X0] :
( ~ sQ14_spl
| leq(nbr_proc,s(X0))
| ~ leq(host(sK11_skl),X0) ),
inference(paramodulation,[status(thm)],[f389,f204]) ).
fof(f835,definition,
( sQ65_spl
<=> setIn(sK11_skl,alive) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f837,plain,
( sQ65_spl
| ~ setIn(sK11_skl,alive) ),
inference(component_clause,[status(thm)],[f835]) ).
fof(f857,plain,
! [X0] : ~ leq(s(s(X0)),X0),
inference(resolution,[status(thm)],[f210,f191]) ).
fof(f873,plain,
! [X0] :
( ~ sQ14_spl
| ~ leq(s(X0),nbr_proc)
| leq(X0,host(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f389,f205]) ).
fof(f874,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| leq(s(X0),X1)
| s(X0) = s(X1) ),
inference(resolution,[status(thm)],[f208,f204]) ).
fof(f992,plain,
( sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f837,f249]) ).
fof(f993,plain,
sQ65_spl,
inference(contradiction_clause,[status(thm)],[f992]) ).
fof(f1073,plain,
! [X0] : ~ leq(host(X0),zero),
inference(resolution,[status(thm)],[f784,f74]) ).
fof(f1238,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f241,f623]) ).
fof(f1239,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1238]) ).
fof(f1367,plain,
leq(nbr_proc,host(sK5_skl)),
inference(forward_demodulation,[status(thm)],[f242,f243]) ).
fof(f1369,plain,
( host(sK5_skl) = nbr_proc
| ~ leq(host(sK5_skl),nbr_proc) ),
inference(resolution,[status(thm)],[f1367,f196]) ).
fof(f1370,definition,
( sQ102_spl
<=> leq(host(sK5_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1372,plain,
( sQ102_spl
| ~ leq(host(sK5_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f1370]) ).
fof(f1373,definition,
( sQ103_spl
<=> host(sK5_skl) = nbr_proc ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1374,plain,
( ~ sQ103_spl
| host(sK5_skl) = nbr_proc ),
inference(component_clause,[status(thm)],[f1373]) ).
fof(f1376,plain,
( sQ103_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f1369,f1370,f1373]) ).
fof(f1377,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1372,f76]) ).
fof(f1378,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f1377]) ).
fof(f1379,plain,
! [X0] :
( leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| ~ setIn(sK11_skl,alive)
| host(X0) = host(sK13_skl)
| ~ leq(s(zero),host(X0))
| leq(host(sK11_skl),host(X0)) ),
inference(resolution,[status(thm)],[f248,f220]) ).
fof(f1380,definition,
! [X0] :
( sQ104_spl
<=> ( leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| host(X0) = host(sK13_skl)
| ~ leq(s(zero),host(X0))
| leq(host(sK11_skl),host(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1381,plain,
! [X0] :
( ~ sQ104_spl
| leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| host(X0) = host(sK13_skl)
| ~ leq(s(zero),host(X0))
| leq(host(sK11_skl),host(X0)) ),
inference(component_clause,[status(thm)],[f1380]) ).
fof(f1383,plain,
( ~ sQ65_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1379,f1380,f835]) ).
fof(f1384,plain,
! [X0] :
( ~ sQ104_spl
| leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| host(X0) = host(sK13_skl)
| leq(host(sK11_skl),host(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1381,f74]) ).
fof(f1386,plain,
( ~ sQ103_spl
| nbr_proc = index(pendack,host(sK4_skl)) ),
inference(backward_demodulation,[status(thm)],[f1374,f242]) ).
fof(f1387,plain,
( sQ15_spl
| ~ sQ103_spl
| ~ leq(nbr_proc,host(sK4_skl)) ),
inference(backward_demodulation,[status(thm)],[f1374,f369]) ).
fof(f1495,plain,
! [X0] :
( leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| host(X0) != host(sK12_skl)
| ~ setIn(X0,alive)
| ~ setIn(sK11_skl,alive) ),
inference(resolution,[status(thm)],[f251,f222]) ).
fof(f1528,definition,
! [X0] :
( sQ125_spl
<=> ( leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| host(X0) != host(sK12_skl)
| ~ setIn(X0,alive) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1529,plain,
! [X0] :
( ~ sQ125_spl
| leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| host(X0) != host(sK12_skl)
| ~ setIn(X0,alive) ),
inference(component_clause,[status(thm)],[f1528]) ).
fof(f1531,plain,
( sQ125_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f1495,f835,f1528]) ).
fof(f1539,plain,
! [X0] :
( ~ sQ125_spl
| ~ sQ14_spl
| leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| host(X0) != nbr_proc
| ~ setIn(X0,alive) ),
inference(forward_demodulation,[status(thm)],[f364,f1529]) ).
fof(f1559,plain,
! [X0] :
( leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| host(X0) != host(sK13_skl)
| ~ setIn(X0,alive)
| ~ setIn(sK11_skl,alive) ),
inference(resolution,[status(thm)],[f252,f222]) ).
fof(f1589,definition,
! [X0] :
( sQ133_spl
<=> ( leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| host(X0) != host(sK13_skl)
| ~ setIn(X0,alive) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1590,plain,
! [X0] :
( ~ sQ133_spl
| leq(index(pendack,host(X0)),host(sK11_skl))
| index(status,host(X0)) != elec_2
| host(X0) != host(sK13_skl)
| ~ setIn(X0,alive) ),
inference(component_clause,[status(thm)],[f1589]) ).
fof(f1592,plain,
( sQ133_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f1559,f835,f1589]) ).
fof(f1684,plain,
! [X0] : ~ leq(s(s(nbr_proc)),host(X0)),
inference(resolution,[status(thm)],[f775,f857]) ).
fof(f1764,definition,
( sQ142_spl
<=> sK11_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1765,plain,
( ~ sQ142_spl
| sK11_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f1764]) ).
fof(f1767,definition,
( sQ143_spl
<=> host(sK11_skl) = host(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1774,definition,
( sQ145_spl
<=> host(sK4_skl) = host(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1776,plain,
( sQ145_spl
| host(sK4_skl) != host(sK4_skl) ),
inference(component_clause,[status(thm)],[f1774]) ).
fof(f1779,plain,
( host(sK4_skl) != host(sK11_skl)
| sK4_skl = sK11_skl ),
inference(resolution,[status(thm)],[f306,f239]) ).
fof(f1783,definition,
( sQ147_spl
<=> host(sK11_skl) = host(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1785,plain,
( sQ147_spl
| host(sK11_skl) != host(sK11_skl) ),
inference(component_clause,[status(thm)],[f1783]) ).
fof(f1787,plain,
( ~ sQ143_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f1779,f1764,f1767]) ).
fof(f1795,plain,
( ~ sQ142_spl
| host(sK4_skl) != host(sK4_skl) ),
inference(backward_demodulation,[status(thm)],[f1765,f247]) ).
fof(f1805,plain,
( ~ sQ142_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1795]) ).
fof(f1806,plain,
~ sQ142_spl,
inference(contradiction_clause,[status(thm)],[f1805]) ).
fof(f1976,definition,
( sQ156_spl
<=> leq(nbr_proc,nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f2506,plain,
( ~ sQ14_spl
| leq(nbr_proc,nbr_proc)
| ~ leq(host(sK11_skl),host(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f389,f791]) ).
fof(f2507,definition,
( sQ172_spl
<=> leq(host(sK11_skl),host(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f2509,plain,
( sQ172_spl
| ~ leq(host(sK11_skl),host(sK11_skl)) ),
inference(component_clause,[status(thm)],[f2507]) ).
fof(f2510,plain,
( ~ sQ14_spl
| sQ156_spl
| ~ sQ172_spl ),
inference(split_clause,[status(thm)],[f2506,f2507,f1976,f363]) ).
fof(f2511,plain,
( sQ172_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2509,f192]) ).
fof(f2512,plain,
sQ172_spl,
inference(contradiction_clause,[status(thm)],[f2511]) ).
fof(f2794,definition,
( sQ181_spl
<=> q_nil = snoc(init(q_nil),last(q_nil)) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f2795,plain,
( ~ sQ181_spl
| q_nil = snoc(init(q_nil),last(q_nil)) ),
inference(component_clause,[status(thm)],[f2794]) ).
fof(f2804,definition,
( sQ182_spl
<=> q_nil = cons(head(q_nil),tail(q_nil)) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2805,plain,
( ~ sQ182_spl
| q_nil = cons(head(q_nil),tail(q_nil)) ),
inference(component_clause,[status(thm)],[f2804]) ).
fof(f2815,plain,
( ~ sQ181_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2795,f134]) ).
fof(f2816,plain,
~ sQ181_spl,
inference(contradiction_clause,[status(thm)],[f2815]) ).
fof(f3002,definition,
( sQ195_spl
<=> leq(zero,zero) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f3004,plain,
( sQ195_spl
| ~ leq(zero,zero) ),
inference(component_clause,[status(thm)],[f3002]) ).
fof(f3035,plain,
( sQ195_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3004,f192]) ).
fof(f3036,plain,
sQ195_spl,
inference(contradiction_clause,[status(thm)],[f3035]) ).
fof(f3175,definition,
! [X0] :
( sQ206_spl
<=> ~ leq(host(X0),host(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f3176,plain,
! [X0] :
( ~ sQ206_spl
| ~ leq(host(X0),host(sK11_skl)) ),
inference(component_clause,[status(thm)],[f3175]) ).
fof(f3825,definition,
( sQ221_spl
<=> host(q_nil) = host(q_nil) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f3827,plain,
( sQ221_spl
| host(q_nil) != host(q_nil) ),
inference(component_clause,[status(thm)],[f3825]) ).
fof(f3830,plain,
( sQ221_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3827]) ).
fof(f3831,plain,
sQ221_spl,
inference(contradiction_clause,[status(thm)],[f3830]) ).
fof(f3839,plain,
( ~ sQ182_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2805,f133]) ).
fof(f3840,plain,
~ sQ182_spl,
inference(contradiction_clause,[status(thm)],[f3839]) ).
fof(f3841,plain,
( sQ147_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1785]) ).
fof(f3842,plain,
sQ147_spl,
inference(contradiction_clause,[status(thm)],[f3841]) ).
fof(f3843,plain,
( sQ145_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1776]) ).
fof(f3844,plain,
sQ145_spl,
inference(contradiction_clause,[status(thm)],[f3843]) ).
fof(f4087,definition,
( sQ230_spl
<=> leq(host(sK11_skl),zero) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f4088,plain,
( ~ sQ230_spl
| leq(host(sK11_skl),zero) ),
inference(component_clause,[status(thm)],[f4087]) ).
fof(f4404,definition,
( sQ245_spl
<=> pidElem(m_Down(q_nil)) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f4406,plain,
( sQ245_spl
| ~ pidElem(m_Down(q_nil)) ),
inference(component_clause,[status(thm)],[f4404]) ).
fof(f4409,plain,
( sQ245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4406,f279]) ).
fof(f4410,plain,
sQ245_spl,
inference(contradiction_clause,[status(thm)],[f4409]) ).
fof(f4967,definition,
( sQ270_spl
<=> m_Down(sK5_skl) = m_Halt(sK0_skl(m_Down(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f4968,plain,
( ~ sQ270_spl
| m_Down(sK5_skl) = m_Halt(sK0_skl(m_Down(sK5_skl))) ),
inference(component_clause,[status(thm)],[f4967]) ).
fof(f4974,plain,
( ~ sQ270_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4968,f89]) ).
fof(f4975,plain,
~ sQ270_spl,
inference(contradiction_clause,[status(thm)],[f4974]) ).
fof(f5012,definition,
! [X0] :
( sQ275_spl
<=> ~ leq(host(X0),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ275_spl])],[split_symbol_definition]) ).
fof(f5013,plain,
! [X0] :
( ~ sQ275_spl
| ~ leq(host(X0),nbr_proc) ),
inference(component_clause,[status(thm)],[f5012]) ).
fof(f5170,definition,
( sQ280_spl
<=> s(zero) = s(s(nbr_proc)) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f5171,plain,
( ~ sQ280_spl
| s(zero) = s(s(nbr_proc)) ),
inference(component_clause,[status(thm)],[f5170]) ).
fof(f5326,plain,
( ~ sQ206_spl
| $false ),
inference(resolution,[status(thm)],[f3176,f192]) ).
fof(f5329,plain,
~ sQ206_spl,
inference(contradiction_clause,[status(thm)],[f5326]) ).
fof(f5367,plain,
( ~ sQ16_spl
| ~ sQ103_spl
| nbr_proc = host(sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f1374,f371]) ).
fof(f6051,plain,
( ~ sQ104_spl
| leq(index(pendack,host(sK4_skl)),host(sK11_skl))
| index(status,host(sK4_skl)) != elec_2
| host(sK4_skl) = host(sK13_skl)
| leq(host(sK11_skl),host(sK4_skl)) ),
inference(resolution,[status(thm)],[f1384,f239]) ).
fof(f6053,definition,
( sQ323_spl
<=> leq(host(sK11_skl),host(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f6054,plain,
( ~ sQ323_spl
| leq(host(sK11_skl),host(sK4_skl)) ),
inference(component_clause,[status(thm)],[f6053]) ).
fof(f6056,definition,
( sQ324_spl
<=> host(sK4_skl) = host(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition]) ).
fof(f6059,definition,
( sQ325_spl
<=> leq(index(pendack,host(sK4_skl)),host(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition]) ).
fof(f6060,plain,
( ~ sQ325_spl
| leq(index(pendack,host(sK4_skl)),host(sK11_skl)) ),
inference(component_clause,[status(thm)],[f6059]) ).
fof(f6062,plain,
( ~ sQ104_spl
| sQ325_spl
| ~ sQ49_spl
| sQ324_spl
| sQ323_spl ),
inference(split_clause,[status(thm)],[f6051,f6053,f6056,f621,f6059,f1380]) ).
fof(f6070,plain,
( ~ sQ325_spl
| ~ sQ103_spl
| leq(nbr_proc,host(sK11_skl)) ),
inference(forward_demodulation,[status(thm)],[f1386,f6060]) ).
fof(f6071,plain,
( ~ sQ325_spl
| ~ sQ103_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6070,f773]) ).
fof(f6072,plain,
( ~ sQ325_spl
| ~ sQ103_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f6071]) ).
fof(f6128,definition,
( sQ333_spl
<=> nbr_proc = host(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition]) ).
fof(f6130,plain,
( sQ333_spl
| nbr_proc != host(sK4_skl) ),
inference(component_clause,[status(thm)],[f6128]) ).
fof(f6256,definition,
( sQ347_spl
<=> leq(host(sK4_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ347_spl])],[split_symbol_definition]) ).
fof(f6258,plain,
( sQ347_spl
| ~ leq(host(sK4_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f6256]) ).
fof(f6265,plain,
( sQ347_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6258,f76]) ).
fof(f6266,plain,
sQ347_spl,
inference(contradiction_clause,[status(thm)],[f6265]) ).
fof(f6267,plain,
( ~ sQ230_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4088,f1073]) ).
fof(f6268,plain,
~ sQ230_spl,
inference(contradiction_clause,[status(thm)],[f6267]) ).
fof(f6550,plain,
( ~ sQ125_spl
| ~ sQ14_spl
| leq(index(pendack,host(sK4_skl)),host(sK11_skl))
| index(status,host(sK4_skl)) != elec_2
| host(sK4_skl) != nbr_proc ),
inference(resolution,[status(thm)],[f1539,f239]) ).
fof(f6552,plain,
( ~ sQ125_spl
| ~ sQ14_spl
| sQ325_spl
| ~ sQ49_spl
| ~ sQ333_spl ),
inference(split_clause,[status(thm)],[f6550,f6128,f621,f6059,f363,f1528]) ).
fof(f6568,definition,
( sQ358_spl
<=> leq(host(sK4_skl),host(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition]) ).
fof(f6658,plain,
( ~ sQ133_spl
| leq(index(pendack,host(sK4_skl)),host(sK11_skl))
| index(status,host(sK4_skl)) != elec_2
| host(sK4_skl) != host(sK13_skl) ),
inference(resolution,[status(thm)],[f1590,f239]) ).
fof(f6660,plain,
( ~ sQ133_spl
| sQ325_spl
| ~ sQ49_spl
| ~ sQ324_spl ),
inference(split_clause,[status(thm)],[f6658,f6056,f621,f6059,f1589]) ).
fof(f6968,plain,
( ~ sQ275_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5013,f76]) ).
fof(f6969,plain,
~ sQ275_spl,
inference(contradiction_clause,[status(thm)],[f6968]) ).
fof(f7104,plain,
! [X0] :
( ~ sQ280_spl
| ~ leq(s(zero),host(X0)) ),
inference(backward_demodulation,[status(thm)],[f5171,f1684]) ).
fof(f7141,plain,
( ~ sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7104,f74]) ).
fof(f7142,plain,
~ sQ280_spl,
inference(contradiction_clause,[status(thm)],[f7141]) ).
fof(f7201,plain,
( ~ sQ323_spl
| leq(s(host(sK11_skl)),host(sK4_skl))
| s(host(sK11_skl)) = s(host(sK4_skl)) ),
inference(resolution,[status(thm)],[f6054,f874]) ).
fof(f7208,plain,
( ~ sQ323_spl
| host(sK4_skl) = host(sK11_skl)
| ~ leq(host(sK4_skl),host(sK11_skl)) ),
inference(resolution,[status(thm)],[f6054,f196]) ).
fof(f7209,definition,
( sQ383_spl
<=> s(host(sK11_skl)) = s(host(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition]) ).
fof(f7210,plain,
( ~ sQ383_spl
| s(host(sK11_skl)) = s(host(sK4_skl)) ),
inference(component_clause,[status(thm)],[f7209]) ).
fof(f7212,definition,
( sQ384_spl
<=> leq(s(host(sK11_skl)),host(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f7213,plain,
( ~ sQ384_spl
| leq(s(host(sK11_skl)),host(sK4_skl)) ),
inference(component_clause,[status(thm)],[f7212]) ).
fof(f7215,plain,
( ~ sQ323_spl
| sQ384_spl
| sQ383_spl ),
inference(split_clause,[status(thm)],[f7201,f7209,f7212,f6053]) ).
fof(f7220,plain,
( ~ sQ323_spl
| sQ143_spl
| ~ sQ358_spl ),
inference(split_clause,[status(thm)],[f7208,f6568,f1767,f6053]) ).
fof(f7221,plain,
( ~ sQ383_spl
| ~ sQ14_spl
| nbr_proc = s(host(sK4_skl)) ),
inference(forward_demodulation,[status(thm)],[f389,f7210]) ).
fof(f7222,plain,
( ~ sQ384_spl
| ~ sQ14_spl
| leq(nbr_proc,host(sK4_skl)) ),
inference(forward_demodulation,[status(thm)],[f389,f7213]) ).
fof(f7223,plain,
( ~ sQ384_spl
| ~ sQ14_spl
| sQ15_spl
| ~ sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7222,f1387]) ).
fof(f7224,plain,
( ~ sQ384_spl
| ~ sQ14_spl
| sQ15_spl
| ~ sQ103_spl ),
inference(contradiction_clause,[status(thm)],[f7223]) ).
fof(f7231,plain,
( ~ sQ383_spl
| ~ sQ14_spl
| ~ leq(nbr_proc,nbr_proc)
| leq(host(sK4_skl),host(sK11_skl)) ),
inference(paramodulation,[status(thm)],[f7221,f873]) ).
fof(f7258,plain,
( ~ sQ383_spl
| ~ sQ14_spl
| ~ sQ156_spl
| sQ358_spl ),
inference(split_clause,[status(thm)],[f7231,f6568,f1976,f363,f7209]) ).
fof(f7487,plain,
( ~ sQ16_spl
| ~ sQ103_spl
| sQ333_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5367,f6130]) ).
fof(f7488,plain,
( ~ sQ16_spl
| ~ sQ103_spl
| sQ333_spl ),
inference(contradiction_clause,[status(thm)],[f7487]) ).
fof(f7489,plain,
$false,
inference(sat_refutation,[status(thm)],[f366,f373,f382,f993,f1239,f1376,f1378,f1383,f1531,f1592,f1787,f1806,f2510,f2512,f2816,f3036,f3831,f3840,f3842,f3844,f4410,f4975,f5329,f6062,f6072,f6266,f6268,f6552,f6660,f6969,f7142,f7215,f7220,f7224,f7258,f7488]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV479+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/15.37 % Computer : n002.cluster.edu
% 0.09/15.37 % Model : x86_64 x86_64
% 0.09/15.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.37 % Memory : 8046.5625MB
% 0.09/15.37 % OS : Linux 6.8.0-71-generic
% 0.09/15.37 % CPULimit : 300
% 0.09/15.37 % WCLimit : 300
% 0.09/15.37 % DateTime : Mon Sep 21 08:55:49 UTC 2026
% 0.09/15.38 % CPUTime :
% 0.09/15.39 % Drodi V4.1.1
% 0.12/16.11 % Refutation found
% 0.12/16.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/16.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.51/16.14 % Elapsed time: 0.743660 seconds
% 0.51/16.14 % CPU time: 5.600978 seconds
% 0.51/16.14 % Total memory used: 166.504 MB
% 0.51/16.14 % Net memory used: 156.701 MB
%------------------------------------------------------------------------------