%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV463+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 : n016.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:47:59 PM UTC 2026
% Result : Theorem 5.07s 1.18s
% Output : CNFRefutation 5.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 53
% Syntax : Number of formulae : 242 ( 76 unt; 34 def)
% Number of atoms : 965 ( 339 equ)
% Maximal formula atoms : 94 ( 3 avg)
% Number of connectives : 1194 ( 471 ~; 377 |; 258 &)
% ( 37 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 44 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 40 ( 38 usr; 35 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 22 con; 0-3 aty)
% Number of variables : 374 ( 350 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [P] : leq(s(zero),host(P)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
leq(s(zero),nbr_proc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [P] : leq(host(P),nbr_proc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X,Y] : m_Down(X) != m_Ldr(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X,Y] : m_Down(X) != m_NormQ(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [Y,Q] : last(snoc(Q,Y)) = Y,
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(f48,axiom,
! [X,Y,Q] :
( elem(X,snoc(Q,Y))
<=> ( elem(X,Q)
| X = 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(f61,axiom,
! [X,Y] :
( leq(Y,X)
| leq(X,Y) ),
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(f67,conjecture,
! [V,W,X,Y] :
( ( queue(host(X)) = cons(m_Ack(W,Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid20) = s(index(pendack,host(Pid0)))
& host(Pid30) = index(pendack,host(Pid0))
& index(status,host(Pid0)) = elec_2
& leq(nbr_proc,s(index(pendack,host(Pid0))))
& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& host(Pid0) = host(Pid30)
& host(Pid0) = nbr_proc
& elem(m_Down(Pid20),queue(host(Pid0)))
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( elem(m_Down(Pid30),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& elem(m_Halt(Pid0),queue(host(Pid20)))
& setIn(Pid0,alive)
& ~ leq(index(pendack,host(Pid0)),host(Z)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& host(Pid0) = host(Pid20)
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z] :
( ( setIn(Z,alive)
& ( index(status,host(Z)) = elec_2
| index(status,host(Z)) = elec_1 ) )
=> index(elid,host(Z)) = Z )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& setIn(Pid0,alive) )
=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
& ! [Z,Pid0] :
( ( elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> leq(host(Z),index(pendack,host(Pid0))) )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( elem(m_Ack(Pid0,Z),queue(host(Pid20)))
=> ~ leq(host(Z),host(Pid0)) )
& ! [Z,Pid0] :
( elem(m_Halt(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_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( ( host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2
& index(elid,host(X)) = W )
=> ( leq(nbr_proc,index(pendack,host(X)))
=> ! [Z] :
( ( host(Z) = host(Y)
| setIn(host(Z),index(acks,host(X))) )
=> ! [V0] :
( host(X) != host(V0)
=> ! [W0,X0,Y0] :
( host(Z) = host(Y0)
=> ( host(X) != host(Y0)
=> ( ( host(X0) = s(index(pendack,host(Y0)))
& host(W0) = index(pendack,host(Y0))
& index(status,host(Y0)) = elec_2
& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
& leq(nbr_proc,s(index(pendack,host(Y0))))
& setIn(Y0,alive) )
=> ~ ( index(status,host(V0)) = norm
& index(ldr,host(V0)) = 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_Ack(W,Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid20) = s(index(pendack,host(Pid0)))
& host(Pid30) = index(pendack,host(Pid0))
& index(status,host(Pid0)) = elec_2
& leq(nbr_proc,s(index(pendack,host(Pid0))))
& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& host(Pid0) = host(Pid30)
& host(Pid0) = nbr_proc
& elem(m_Down(Pid20),queue(host(Pid0)))
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( elem(m_Down(Pid30),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& elem(m_Halt(Pid0),queue(host(Pid20)))
& setIn(Pid0,alive)
& ~ leq(index(pendack,host(Pid0)),host(Z)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& host(Pid0) = host(Pid20)
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z] :
( ( setIn(Z,alive)
& ( index(status,host(Z)) = elec_2
| index(status,host(Z)) = elec_1 ) )
=> index(elid,host(Z)) = Z )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& setIn(Pid0,alive) )
=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
& ! [Z,Pid0] :
( ( elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> leq(host(Z),index(pendack,host(Pid0))) )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( elem(m_Ack(Pid0,Z),queue(host(Pid20)))
=> ~ leq(host(Z),host(Pid0)) )
& ! [Z,Pid0] :
( elem(m_Halt(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_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( ( host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2
& index(elid,host(X)) = W )
=> ( leq(nbr_proc,index(pendack,host(X)))
=> ! [Z] :
( ( host(Z) = host(Y)
| setIn(host(Z),index(acks,host(X))) )
=> ! [V0] :
( host(X) != host(V0)
=> ! [W0,X0,Y0] :
( host(Z) = host(Y0)
=> ( host(X) != host(Y0)
=> ( ( host(X0) = s(index(pendack,host(Y0)))
& host(W0) = index(pendack,host(Y0))
& index(status,host(Y0)) = elec_2
& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
& leq(nbr_proc,s(index(pendack,host(Y0))))
& setIn(Y0,alive) )
=> ~ ( index(status,host(V0)) = norm
& index(ldr,host(V0)) = 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(f75,plain,
leq(s(zero),nbr_proc),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f76,plain,
! [X0] : leq(host(X0),nbr_proc),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f83,plain,
! [X0,X1,X2] : m_Ack(X0,X1) != m_Halt(X2),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f84,plain,
! [X0,X1,X2] : m_Ack(X0,X1) != m_Down(X2),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f86,plain,
! [X0,X1,X2] : m_Ack(X0,X1) != m_Ldr(X2),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f87,plain,
! [X0,X1,X2] : m_Ack(X0,X1) != m_NormQ(X2),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f90,plain,
! [X0,X1] : m_Down(X0) != m_Ldr(X1),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f92,plain,
! [X0,X1] : m_Down(X0) != m_NormQ(X1),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f129,plain,
! [X0,X1] : last(snoc(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f134,plain,
! [X0,X1] : q_nil != snoc(X0,X1),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f143,plain,
! [X,Y,Q] :
( ( ( ~ elem(X,Q)
& X != Y )
| elem(X,snoc(Q,Y)) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,snoc(Q,Y)) ) ),
inference(NNF_transformation,[status(thm)],[f48]) ).
fof(f144,plain,
( ! [X,Y,Q] :
( ( ~ elem(X,Q)
& X != Y )
| elem(X,snoc(Q,Y)) )
& ! [X,Y,Q] :
( elem(X,Q)
| X = Y
| ~ elem(X,snoc(Q,Y)) ) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f145,plain,
! [X0,X1,X2] :
( elem(X0,X1)
| X0 = X2
| ~ elem(X0,snoc(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
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(f151,plain,
! [X0] :
( X0 = m_Down(sK1_skl(X0))
| X0 = m_Halt(sK0_skl(X0))
| ~ 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(f193,plain,
! [X0,X1] :
( leq(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
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(f212,plain,
? [V,W,X,Y] :
( ? [Z] :
( ? [V0] :
( ? [W0,X0,Y0] :
( index(status,host(V0)) = norm
& index(ldr,host(V0)) = host(V0)
& setIn(V0,alive)
& host(X0) = s(index(pendack,host(Y0)))
& host(W0) = index(pendack,host(Y0))
& index(status,host(Y0)) = elec_2
& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
& leq(nbr_proc,s(index(pendack,host(Y0))))
& setIn(Y0,alive)
& host(X) != host(Y0)
& host(Z) = host(Y0) )
& host(X) != host(V0) )
& ( host(Z) = host(Y)
| 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
& index(elid,host(X)) = W
& setIn(X,alive)
& queue(host(X)) = cons(m_Ack(W,Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| host(Pid20) != s(index(pendack,host(Pid0)))
| host(Pid30) != index(pendack,host(Pid0))
| index(status,host(Pid0)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(Pid0))))
| ~ elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ elem(m_Down(Pid30),queue(host(Z)))
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_1
| host(Pid0) != host(Pid30)
| host(Pid0) != nbr_proc
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ? [V0] :
( V0 != host(Pid20)
& ~ setIn(V0,index(down,host(Pid0)))
& leq(s(zero),V0)
& ~ leq(host(Pid0),V0) ) )
& ! [Z,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_2
| ~ elem(m_Halt(Pid0),queue(host(Pid20)))
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid0] :
( ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0)))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [Z,Pid20,Pid0] :
( ~ elem(m_Ack(Z,Pid20),queue(host(Z)))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| host(Pid0) != host(Pid20)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [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) )
& ! [Z] :
( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ! [Z,Pid0] :
( ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| index(status,host(Pid0)) != elec_1
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(host(Z),index(pendack,host(Pid0)))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid20,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid20))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Halt(Pid0),queue(host(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,
? [W,X,Y] :
( ? [Z] :
( ? [V0] :
( ? [Y0] :
( index(status,host(V0)) = norm
& index(ldr,host(V0)) = host(V0)
& setIn(V0,alive)
& ? [X0] :
( host(X0) = s(index(pendack,host(Y0)))
& ? [W0] :
( host(W0) = index(pendack,host(Y0))
& index(status,host(Y0)) = elec_2
& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
& leq(nbr_proc,s(index(pendack,host(Y0))))
& setIn(Y0,alive) ) )
& host(X) != host(Y0)
& host(Z) = host(Y0) )
& host(X) != host(V0) )
& ( host(Z) = host(Y)
| 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
& index(elid,host(X)) = W
& setIn(X,alive)
& ? [V] : queue(host(X)) = cons(m_Ack(W,Y),V)
& ( ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive) )
| ! [Pid20,Pid0] :
( host(Pid20) != s(index(pendack,host(Pid0)))
| ! [Pid30] :
( host(Pid30) != index(pendack,host(Pid0))
| index(status,host(Pid0)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(Pid0))))
| ~ elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) ) ) )
& ! [Pid30] :
( ! [Z] :
( ~ elem(m_Down(Pid30),queue(host(Z)))
| ~ setIn(Z,alive) )
| ! [Pid0] :
( index(status,host(Pid0)) != elec_1
| host(Pid0) != host(Pid30)
| host(Pid0) != nbr_proc
| ! [Pid20] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ? [V0] :
( V0 != host(Pid20)
& ~ setIn(V0,index(down,host(Pid0)))
& leq(s(zero),V0)
& ~ leq(host(Pid0),V0) ) ) ) )
& ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| ! [Pid0] :
( index(status,host(Pid0)) != elec_2
| ! [Pid20] : ~ elem(m_Halt(Pid0),queue(host(Pid20)))
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Z)) ) )
& ! [Z,Pid0] :
( ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0)))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [Z,Pid20] :
( ~ elem(m_Ack(Z,Pid20),queue(host(Z)))
| ! [Pid0] :
( index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| host(Pid0) != host(Pid20)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [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) ) ) )
& ! [Z] :
( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ! [Pid0] :
( ! [Z] : ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| index(status,host(Pid0)) != elec_1
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(host(Z),index(pendack,host(Pid0)))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ! [Pid20] : ~ elem(m_Ack(Pid0,Z),queue(host(Pid20))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Halt(Pid0),queue(host(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,
( index(status,host(sK10_skl)) = norm
& index(ldr,host(sK10_skl)) = host(sK10_skl)
& setIn(sK10_skl,alive)
& host(sK12_skl) = s(index(pendack,host(sK11_skl)))
& host(sK13_skl) = index(pendack,host(sK11_skl))
& index(status,host(sK11_skl)) = elec_2
& elem(m_Ack(sK11_skl,sK13_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl)))
& elem(m_Down(sK12_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl)))
& leq(nbr_proc,s(index(pendack,host(sK11_skl))))
& setIn(sK11_skl,alive)
& host(sK5_skl) != host(sK11_skl)
& host(sK9_skl) = host(sK11_skl)
& host(sK5_skl) != host(sK10_skl)
& ( host(sK9_skl) = host(sK6_skl)
| setIn(host(sK9_skl),index(acks,host(sK5_skl))) )
& leq(nbr_proc,index(pendack,host(sK5_skl)))
& host(sK6_skl) = index(pendack,host(sK5_skl))
& index(status,host(sK5_skl)) = elec_2
& index(elid,host(sK5_skl)) = sK4_skl
& setIn(sK5_skl,alive)
& queue(host(sK5_skl)) = cons(m_Ack(sK4_skl,sK6_skl),sK8_skl)
& ( ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive) )
| ! [Pid20,Pid0] :
( host(Pid20) != s(index(pendack,host(Pid0)))
| ! [Pid30] :
( host(Pid30) != index(pendack,host(Pid0))
| index(status,host(Pid0)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(Pid0))))
| ~ elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) ) ) )
& ! [Pid30] :
( ! [Z] :
( ~ elem(m_Down(Pid30),queue(host(Z)))
| ~ setIn(Z,alive) )
| ! [Pid0] :
( index(status,host(Pid0)) != elec_1
| host(Pid0) != host(Pid30)
| host(Pid0) != nbr_proc
| ! [Pid20] :
( ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ( sK7_skl(Pid20,Pid0,Pid30) != host(Pid20)
& ~ setIn(sK7_skl(Pid20,Pid0,Pid30),index(down,host(Pid0)))
& leq(s(zero),sK7_skl(Pid20,Pid0,Pid30))
& ~ leq(host(Pid0),sK7_skl(Pid20,Pid0,Pid30)) ) ) ) )
& ! [Z] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| ! [Pid0] :
( index(status,host(Pid0)) != elec_2
| ! [Pid20] : ~ elem(m_Halt(Pid0),queue(host(Pid20)))
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Z)) ) )
& ! [Z,Pid0] :
( ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0)))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [Z,Pid20] :
( ~ elem(m_Ack(Z,Pid20),queue(host(Z)))
| ! [Pid0] :
( index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| host(Pid0) != host(Pid20)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [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) ) ) )
& ! [Z] :
( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ! [Pid0] :
( ! [Z] : ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| index(status,host(Pid0)) != elec_1
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(host(Z),index(pendack,host(Pid0)))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ! [Pid20] : ~ elem(m_Ack(Pid0,Z),queue(host(Pid20))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Halt(Pid0),queue(host(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(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]) ).
fof(f233,plain,
! [X0,X1,X2,X3] :
( index(status,host(X3)) != norm
| index(ldr,host(X3)) != host(X3)
| ~ setIn(X3,alive)
| host(X1) != s(index(pendack,host(X0)))
| host(X2) != index(pendack,host(X0))
| index(status,host(X0)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(X0))))
| ~ elem(m_Ack(X0,X2),queue(host(X0)))
| ~ elem(m_Down(X1),queue(host(X0)))
| ~ setIn(X0,alive) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f242,plain,
host(sK9_skl) = host(sK11_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f244,plain,
setIn(sK11_skl,alive),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f245,plain,
leq(nbr_proc,s(index(pendack,host(sK11_skl)))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f246,plain,
elem(m_Down(sK12_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f247,plain,
elem(m_Ack(sK11_skl,sK13_skl),snoc(queue(host(sK11_skl)),m_Ldr(sK5_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f248,plain,
index(status,host(sK11_skl)) = elec_2,
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f249,plain,
host(sK13_skl) = index(pendack,host(sK11_skl)),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f250,plain,
host(sK12_skl) = s(index(pendack,host(sK11_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f251,plain,
setIn(sK10_skl,alive),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f252,plain,
index(ldr,host(sK10_skl)) = host(sK10_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f253,plain,
index(status,host(sK10_skl)) = norm,
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f254,definition,
! [X0,X1,X2] :
( sQ0_spl
<=> ( host(X1) != s(index(pendack,host(X0)))
| host(X2) != index(pendack,host(X0))
| index(status,host(X0)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(X0))))
| ~ elem(m_Ack(X0,X2),queue(host(X0)))
| ~ elem(m_Down(X1),queue(host(X0)))
| ~ setIn(X0,alive) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f255,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| host(X1) != s(index(pendack,host(X0)))
| host(X2) != index(pendack,host(X0))
| index(status,host(X0)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(X0))))
| ~ elem(m_Ack(X0,X2),queue(host(X0)))
| ~ elem(m_Down(X1),queue(host(X0)))
| ~ setIn(X0,alive) ),
inference(component_clause,[status(thm)],[f254]) ).
fof(f257,definition,
! [X3] :
( sQ1_spl
<=> ( index(status,host(X3)) != norm
| index(ldr,host(X3)) != host(X3)
| ~ setIn(X3,alive) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f258,plain,
! [X0] :
( ~ sQ1_spl
| index(status,host(X0)) != norm
| index(ldr,host(X0)) != host(X0)
| ~ setIn(X0,alive) ),
inference(component_clause,[status(thm)],[f257]) ).
fof(f260,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f233,f254,f257]) ).
fof(f308,definition,
( sQ6_spl
<=> setIn(sK11_skl,alive) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f310,plain,
( sQ6_spl
| ~ setIn(sK11_skl,alive) ),
inference(component_clause,[status(thm)],[f308]) ).
fof(f315,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f310,f244]) ).
fof(f316,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f315]) ).
fof(f318,plain,
! [X0] : leq(X0,s(X0)),
inference(resolution,[status(thm)],[f193,f191]) ).
fof(f451,plain,
index(status,host(sK9_skl)) = elec_2,
inference(forward_demodulation,[status(thm)],[f242,f248]) ).
fof(f459,definition,
( sQ19_spl
<=> index(status,host(sK11_skl)) = elec_2 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ19_spl
| index(status,host(sK11_skl)) != elec_2 ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f491,plain,
! [X0,X1] :
( leq(s(zero),X1)
| ~ leq(host(X0),X1) ),
inference(resolution,[status(thm)],[f201,f74]) ).
fof(f492,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ leq(s(X0),X1) ),
inference(resolution,[status(thm)],[f201,f318]) ).
fof(f494,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| leq(X2,X1)
| ~ leq(X0,X1) ),
inference(resolution,[status(thm)],[f201,f193]) ).
fof(f585,plain,
( sQ19_spl
| index(status,host(sK9_skl)) != elec_2 ),
inference(forward_demodulation,[status(thm)],[f242,f461]) ).
fof(f586,plain,
( sQ19_spl
| elec_2 != elec_2 ),
inference(forward_demodulation,[status(thm)],[f451,f585]) ).
fof(f587,plain,
( sQ19_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f586]) ).
fof(f588,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f587]) ).
fof(f789,plain,
leq(nbr_proc,s(index(pendack,host(sK9_skl)))),
inference(forward_demodulation,[status(thm)],[f242,f245]) ).
fof(f806,plain,
elem(m_Down(sK12_skl),snoc(queue(host(sK9_skl)),m_Ldr(sK5_skl))),
inference(forward_demodulation,[status(thm)],[f242,f246]) ).
fof(f807,plain,
( elem(m_Down(sK12_skl),queue(host(sK9_skl)))
| m_Down(sK12_skl) = m_Ldr(sK5_skl) ),
inference(resolution,[status(thm)],[f806,f145]) ).
fof(f810,definition,
( sQ50_spl
<=> m_Down(sK12_skl) = m_Ldr(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f811,plain,
( ~ sQ50_spl
| m_Down(sK12_skl) = m_Ldr(sK5_skl) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f813,definition,
( sQ51_spl
<=> elem(m_Down(sK12_skl),queue(host(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f814,plain,
( ~ sQ51_spl
| elem(m_Down(sK12_skl),queue(host(sK9_skl))) ),
inference(component_clause,[status(thm)],[f813]) ).
fof(f816,plain,
( sQ51_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f807,f810,f813]) ).
fof(f817,plain,
( ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f811,f90]) ).
fof(f818,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f817]) ).
fof(f896,plain,
elem(m_Ack(sK11_skl,sK13_skl),snoc(queue(host(sK9_skl)),m_Ldr(sK5_skl))),
inference(forward_demodulation,[status(thm)],[f242,f247]) ).
fof(f897,plain,
( elem(m_Ack(sK11_skl,sK13_skl),queue(host(sK9_skl)))
| m_Ack(sK11_skl,sK13_skl) = m_Ldr(sK5_skl) ),
inference(resolution,[status(thm)],[f896,f145]) ).
fof(f900,definition,
( sQ65_spl
<=> m_Ack(sK11_skl,sK13_skl) = m_Ldr(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f901,plain,
( ~ sQ65_spl
| m_Ack(sK11_skl,sK13_skl) = m_Ldr(sK5_skl) ),
inference(component_clause,[status(thm)],[f900]) ).
fof(f903,definition,
( sQ66_spl
<=> elem(m_Ack(sK11_skl,sK13_skl),queue(host(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f904,plain,
( ~ sQ66_spl
| elem(m_Ack(sK11_skl,sK13_skl),queue(host(sK9_skl))) ),
inference(component_clause,[status(thm)],[f903]) ).
fof(f906,plain,
( sQ66_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f897,f900,f903]) ).
fof(f907,plain,
( ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f901,f86]) ).
fof(f908,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f907]) ).
fof(f909,plain,
leq(nbr_proc,s(host(sK13_skl))),
inference(backward_demodulation,[status(thm)],[f910,f789]) ).
fof(f910,plain,
host(sK13_skl) = index(pendack,host(sK9_skl)),
inference(forward_demodulation,[status(thm)],[f242,f249]) ).
fof(f930,plain,
host(sK12_skl) = s(index(pendack,host(sK9_skl))),
inference(forward_demodulation,[status(thm)],[f242,f250]) ).
fof(f931,plain,
host(sK12_skl) = s(host(sK13_skl)),
inference(forward_demodulation,[status(thm)],[f910,f930]) ).
fof(f942,plain,
! [X0,X1] :
( ~ sQ0_spl
| host(X0) != s(index(pendack,host(sK11_skl)))
| host(X1) != index(pendack,host(sK11_skl))
| index(status,host(sK11_skl)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(sK11_skl))))
| ~ elem(m_Ack(sK11_skl,X1),queue(host(sK11_skl)))
| ~ elem(m_Down(X0),queue(host(sK9_skl)))
| ~ setIn(sK11_skl,alive) ),
inference(paramodulation,[status(thm)],[f242,f255]) ).
fof(f953,definition,
! [X0] :
( sQ74_spl
<=> ( host(X0) != s(index(pendack,host(sK11_skl)))
| ~ elem(m_Down(X0),queue(host(sK9_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f954,plain,
! [X0] :
( ~ sQ74_spl
| host(X0) != s(index(pendack,host(sK11_skl)))
| ~ elem(m_Down(X0),queue(host(sK9_skl))) ),
inference(component_clause,[status(thm)],[f953]) ).
fof(f956,definition,
! [X1] :
( sQ75_spl
<=> ( host(X1) != index(pendack,host(sK11_skl))
| ~ elem(m_Ack(sK11_skl,X1),queue(host(sK11_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f957,plain,
! [X0] :
( ~ sQ75_spl
| host(X0) != index(pendack,host(sK11_skl))
| ~ elem(m_Ack(sK11_skl,X0),queue(host(sK11_skl))) ),
inference(component_clause,[status(thm)],[f956]) ).
fof(f959,definition,
( sQ76_spl
<=> leq(nbr_proc,s(index(pendack,host(sK11_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f961,plain,
( sQ76_spl
| ~ leq(nbr_proc,s(index(pendack,host(sK11_skl)))) ),
inference(component_clause,[status(thm)],[f959]) ).
fof(f962,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| ~ sQ76_spl
| sQ75_spl
| sQ74_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f942,f308,f953,f956,f959,f459,f254]) ).
fof(f963,plain,
( sQ76_spl
| ~ leq(nbr_proc,s(index(pendack,host(sK9_skl)))) ),
inference(forward_demodulation,[status(thm)],[f242,f961]) ).
fof(f964,plain,
( sQ76_spl
| ~ leq(nbr_proc,s(host(sK13_skl))) ),
inference(forward_demodulation,[status(thm)],[f910,f963]) ).
fof(f965,plain,
( sQ76_spl
| ~ leq(nbr_proc,host(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f931,f964]) ).
fof(f1010,plain,
leq(nbr_proc,host(sK12_skl)),
inference(forward_demodulation,[status(thm)],[f931,f909]) ).
fof(f1011,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1010,f965]) ).
fof(f1012,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f1011]) ).
fof(f1013,plain,
! [X0] :
( ~ sQ74_spl
| host(X0) != s(index(pendack,host(sK9_skl)))
| ~ elem(m_Down(X0),queue(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f242,f954]) ).
fof(f1014,plain,
! [X0] :
( ~ sQ74_spl
| host(X0) != s(host(sK13_skl))
| ~ elem(m_Down(X0),queue(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f910,f1013]) ).
fof(f1015,plain,
! [X0] :
( ~ sQ74_spl
| host(X0) != host(sK12_skl)
| ~ elem(m_Down(X0),queue(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f931,f1014]) ).
fof(f1035,plain,
( nbr_proc = host(sK12_skl)
| ~ leq(host(sK12_skl),nbr_proc) ),
inference(resolution,[status(thm)],[f1010,f196]) ).
fof(f1036,definition,
( sQ84_spl
<=> leq(host(sK12_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1038,plain,
( sQ84_spl
| ~ leq(host(sK12_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f1036]) ).
fof(f1039,definition,
( sQ85_spl
<=> nbr_proc = host(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1040,plain,
( ~ sQ85_spl
| nbr_proc = host(sK12_skl) ),
inference(component_clause,[status(thm)],[f1039]) ).
fof(f1042,plain,
( sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f1035,f1036,f1039]) ).
fof(f1043,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1038,f76]) ).
fof(f1044,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f1043]) ).
fof(f1169,plain,
leq(zero,nbr_proc),
inference(resolution,[status(thm)],[f492,f75]) ).
fof(f1335,plain,
! [X0] :
( leq(zero,X0)
| ~ leq(nbr_proc,X0) ),
inference(resolution,[status(thm)],[f1169,f201]) ).
fof(f1752,plain,
! [X0] :
( ~ sQ75_spl
| host(X0) != index(pendack,host(sK11_skl))
| ~ elem(m_Ack(sK11_skl,X0),queue(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f242,f957]) ).
fof(f1753,plain,
! [X0] :
( ~ sQ75_spl
| host(X0) != index(pendack,host(sK9_skl))
| ~ elem(m_Ack(sK11_skl,X0),queue(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f242,f1752]) ).
fof(f1754,plain,
! [X0] :
( ~ sQ75_spl
| host(X0) != host(sK13_skl)
| ~ elem(m_Ack(sK11_skl,X0),queue(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f910,f1753]) ).
fof(f2124,definition,
( sQ158_spl
<=> leq(zero,nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition]) ).
fof(f2209,definition,
( sQ164_spl
<=> leq(nbr_proc,nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2211,plain,
( sQ164_spl
| ~ leq(nbr_proc,nbr_proc) ),
inference(component_clause,[status(thm)],[f2209]) ).
fof(f2368,plain,
! [X0] :
( leq(zero,X0)
| leq(X0,nbr_proc) ),
inference(resolution,[status(thm)],[f494,f1169]) ).
fof(f2392,definition,
! [X0] :
( sQ172_spl
<=> pidElem(X0) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f2393,plain,
! [X0] :
( ~ sQ172_spl
| pidElem(X0) ),
inference(component_clause,[status(thm)],[f2392]) ).
fof(f2473,plain,
( ~ sQ1_spl
| index(status,host(sK10_skl)) != norm
| index(ldr,host(sK10_skl)) != host(sK10_skl) ),
inference(resolution,[status(thm)],[f258,f251]) ).
fof(f2482,definition,
( sQ178_spl
<=> index(ldr,host(sK10_skl)) = host(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f2484,plain,
( sQ178_spl
| index(ldr,host(sK10_skl)) != host(sK10_skl) ),
inference(component_clause,[status(thm)],[f2482]) ).
fof(f2485,definition,
( sQ179_spl
<=> index(status,host(sK10_skl)) = norm ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f2487,plain,
( sQ179_spl
| index(status,host(sK10_skl)) != norm ),
inference(component_clause,[status(thm)],[f2485]) ).
fof(f2488,plain,
( ~ sQ1_spl
| ~ sQ179_spl
| ~ sQ178_spl ),
inference(split_clause,[status(thm)],[f2473,f2482,f2485,f257]) ).
fof(f2497,plain,
( sQ179_spl
| norm != norm ),
inference(forward_demodulation,[status(thm)],[f253,f2487]) ).
fof(f2498,plain,
( sQ179_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2497]) ).
fof(f2499,plain,
sQ179_spl,
inference(contradiction_clause,[status(thm)],[f2498]) ).
fof(f2500,plain,
( sQ178_spl
| host(sK10_skl) != host(sK10_skl) ),
inference(forward_demodulation,[status(thm)],[f252,f2484]) ).
fof(f2501,plain,
( sQ178_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2500]) ).
fof(f2502,plain,
sQ178_spl,
inference(contradiction_clause,[status(thm)],[f2501]) ).
fof(f2511,plain,
! [X0] :
( ~ sQ172_spl
| X0 = m_Down(sK1_skl(X0))
| X0 = m_Halt(sK0_skl(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f151,f2393]) ).
fof(f2532,definition,
( sQ182_spl
<=> leq(host(sK9_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2534,plain,
( sQ182_spl
| ~ leq(host(sK9_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f2532]) ).
fof(f2541,plain,
( sQ182_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2534,f76]) ).
fof(f2542,plain,
sQ182_spl,
inference(contradiction_clause,[status(thm)],[f2541]) ).
fof(f2629,definition,
( sQ198_spl
<=> s(zero) = s(nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f2630,plain,
( ~ sQ198_spl
| s(zero) = s(nbr_proc) ),
inference(component_clause,[status(thm)],[f2629]) ).
fof(f2654,definition,
( sQ202_spl
<=> leq(host(sK13_skl),host(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f2656,plain,
( sQ202_spl
| ~ leq(host(sK13_skl),host(sK13_skl)) ),
inference(component_clause,[status(thm)],[f2654]) ).
fof(f2658,definition,
( sQ203_spl
<=> leq(host(sK13_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2660,plain,
( sQ203_spl
| ~ leq(host(sK13_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f2658]) ).
fof(f2662,definition,
( sQ204_spl
<=> leq(host(sK13_skl),index(pendack,host(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f2664,plain,
( sQ204_spl
| ~ leq(host(sK13_skl),index(pendack,host(sK9_skl))) ),
inference(component_clause,[status(thm)],[f2662]) ).
fof(f2679,plain,
( sQ204_spl
| ~ leq(host(sK13_skl),host(sK13_skl)) ),
inference(forward_demodulation,[status(thm)],[f910,f2664]) ).
fof(f2680,plain,
( sQ204_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2679,f192]) ).
fof(f2681,plain,
sQ204_spl,
inference(contradiction_clause,[status(thm)],[f2680]) ).
fof(f2682,plain,
( sQ203_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2660,f76]) ).
fof(f2683,plain,
sQ203_spl,
inference(contradiction_clause,[status(thm)],[f2682]) ).
fof(f2684,plain,
( sQ202_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2656,f192]) ).
fof(f2685,plain,
sQ202_spl,
inference(contradiction_clause,[status(thm)],[f2684]) ).
fof(f2688,plain,
! [X0,X1] :
( ~ sQ172_spl
| m_Ack(X0,X1) = m_Halt(sK0_skl(m_Ack(X0,X1))) ),
inference(resolution,[status(thm)],[f2511,f84]) ).
fof(f2709,plain,
( ~ sQ172_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2688,f83]) ).
fof(f2710,plain,
~ sQ172_spl,
inference(contradiction_clause,[status(thm)],[f2709]) ).
fof(f2781,definition,
( sQ215_spl
<=> leq(index(pendack,host(sK9_skl)),host(sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f2783,plain,
( sQ215_spl
| ~ leq(index(pendack,host(sK9_skl)),host(sK13_skl)) ),
inference(component_clause,[status(thm)],[f2781]) ).
fof(f2799,plain,
( sQ215_spl
| ~ leq(host(sK13_skl),host(sK13_skl)) ),
inference(forward_demodulation,[status(thm)],[f910,f2783]) ).
fof(f2800,plain,
( sQ215_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2799,f192]) ).
fof(f2801,plain,
sQ215_spl,
inference(contradiction_clause,[status(thm)],[f2800]) ).
fof(f2997,definition,
( sQ233_spl
<=> m_Down(sK12_skl) = last(snoc(queue(s(zero)),m_Ldr(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f2998,plain,
( ~ sQ233_spl
| m_Down(sK12_skl) = last(snoc(queue(s(zero)),m_Ldr(sK4_skl))) ),
inference(component_clause,[status(thm)],[f2997]) ).
fof(f3003,definition,
( sQ235_spl
<=> snoc(queue(s(zero)),m_Ldr(sK4_skl)) = q_nil ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f3004,plain,
( ~ sQ235_spl
| snoc(queue(s(zero)),m_Ldr(sK4_skl)) = q_nil ),
inference(component_clause,[status(thm)],[f3003]) ).
fof(f3007,plain,
( ~ sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3004,f134]) ).
fof(f3008,plain,
~ sQ235_spl,
inference(contradiction_clause,[status(thm)],[f3007]) ).
fof(f3010,plain,
( ~ sQ233_spl
| m_Down(sK12_skl) = m_Ldr(sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f129,f2998]) ).
fof(f3011,plain,
( ~ sQ233_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3010,f90]) ).
fof(f3012,plain,
~ sQ233_spl,
inference(contradiction_clause,[status(thm)],[f3011]) ).
fof(f3036,plain,
( ~ sQ198_spl
| ~ leq(s(zero),nbr_proc) ),
inference(paramodulation,[status(thm)],[f2630,f191]) ).
fof(f3039,plain,
( ~ sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3036,f75]) ).
fof(f3040,plain,
~ sQ198_spl,
inference(contradiction_clause,[status(thm)],[f3039]) ).
fof(f3949,definition,
! [X0] :
( sQ266_spl
<=> m_Down(sK12_skl) = X0 ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f3950,plain,
! [X0] :
( ~ sQ266_spl
| m_Down(sK12_skl) = X0 ),
inference(component_clause,[status(thm)],[f3949]) ).
fof(f4005,plain,
( ~ sQ266_spl
| $false ),
inference(resolution,[status(thm)],[f3950,f92]) ).
fof(f4034,plain,
~ sQ266_spl,
inference(contradiction_clause,[status(thm)],[f4005]) ).
fof(f4039,definition,
! [X0] :
( sQ274_spl
<=> m_Ack(sK11_skl,sK13_skl) = X0 ),
introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition]) ).
fof(f4040,plain,
! [X0] :
( ~ sQ274_spl
| m_Ack(sK11_skl,sK13_skl) = X0 ),
inference(component_clause,[status(thm)],[f4039]) ).
fof(f4048,plain,
( ~ sQ274_spl
| $false ),
inference(resolution,[status(thm)],[f4040,f87]) ).
fof(f4072,plain,
~ sQ274_spl,
inference(contradiction_clause,[status(thm)],[f4048]) ).
fof(f4164,definition,
( sQ284_spl
<=> leq(index(pendack,host(sK9_skl)),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f4166,plain,
( sQ284_spl
| ~ leq(index(pendack,host(sK9_skl)),nbr_proc) ),
inference(component_clause,[status(thm)],[f4164]) ).
fof(f4186,plain,
( sQ284_spl
| ~ leq(host(sK13_skl),nbr_proc) ),
inference(forward_demodulation,[status(thm)],[f910,f4166]) ).
fof(f4187,plain,
( sQ284_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4186,f76]) ).
fof(f4188,plain,
sQ284_spl,
inference(contradiction_clause,[status(thm)],[f4187]) ).
fof(f4189,plain,
( sQ164_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2211,f192]) ).
fof(f4190,plain,
sQ164_spl,
inference(contradiction_clause,[status(thm)],[f4189]) ).
fof(f4315,plain,
! [X0] :
( ~ sQ74_spl
| ~ sQ85_spl
| host(X0) != nbr_proc
| ~ elem(m_Down(X0),queue(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f1040,f1015]) ).
fof(f4316,plain,
( ~ sQ51_spl
| ~ sQ74_spl
| ~ sQ85_spl
| host(sK12_skl) != nbr_proc ),
inference(resolution,[status(thm)],[f4315,f814]) ).
fof(f4317,plain,
( ~ sQ51_spl
| ~ sQ74_spl
| ~ sQ85_spl
| nbr_proc != nbr_proc ),
inference(forward_demodulation,[status(thm)],[f1040,f4316]) ).
fof(f4318,plain,
( ~ sQ51_spl
| ~ sQ74_spl
| ~ sQ85_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4317]) ).
fof(f4319,plain,
( ~ sQ51_spl
| ~ sQ74_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f4318]) ).
fof(f5829,definition,
( sQ357_spl
<=> m_Ack(sK4_skl,sK13_skl) = last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ357_spl])],[split_symbol_definition]) ).
fof(f5830,plain,
( ~ sQ357_spl
| m_Ack(sK4_skl,sK13_skl) = last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl))) ),
inference(component_clause,[status(thm)],[f5829]) ).
fof(f5843,plain,
( ~ sQ357_spl
| m_Ack(sK4_skl,sK13_skl) = m_Ldr(sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f129,f5830]) ).
fof(f5844,plain,
( ~ sQ357_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5843,f86]) ).
fof(f5845,plain,
~ sQ357_spl,
inference(contradiction_clause,[status(thm)],[f5844]) ).
fof(f5943,definition,
( sQ361_spl
<=> m_Ack(sK10_skl,sK13_skl) = m_Ldr(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition]) ).
fof(f5944,plain,
( ~ sQ361_spl
| m_Ack(sK10_skl,sK13_skl) = m_Ldr(sK4_skl) ),
inference(component_clause,[status(thm)],[f5943]) ).
fof(f5950,definition,
( sQ363_spl
<=> m_Ack(sK10_skl,sK13_skl) = last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f5951,plain,
( ~ sQ363_spl
| m_Ack(sK10_skl,sK13_skl) = last(snoc(queue(host(sK9_skl)),m_Ldr(sK4_skl))) ),
inference(component_clause,[status(thm)],[f5950]) ).
fof(f5964,plain,
( ~ sQ361_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5944,f86]) ).
fof(f5965,plain,
~ sQ361_spl,
inference(contradiction_clause,[status(thm)],[f5964]) ).
fof(f5966,plain,
( ~ sQ363_spl
| m_Ack(sK10_skl,sK13_skl) = m_Ldr(sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f129,f5951]) ).
fof(f5967,plain,
( ~ sQ363_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5966,f86]) ).
fof(f5968,plain,
~ sQ363_spl,
inference(contradiction_clause,[status(thm)],[f5967]) ).
fof(f6200,plain,
( leq(zero,nbr_proc)
| leq(zero,nbr_proc) ),
inference(resolution,[status(thm)],[f2368,f1335]) ).
fof(f6228,plain,
sQ158_spl,
inference(split_clause,[status(thm)],[f6200,f2124]) ).
fof(f6366,definition,
( sQ389_spl
<=> leq(nbr_proc,s(nbr_proc)) ),
introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition]) ).
fof(f6368,plain,
( sQ389_spl
| ~ leq(nbr_proc,s(nbr_proc)) ),
inference(component_clause,[status(thm)],[f6366]) ).
fof(f6376,plain,
( sQ389_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6368,f318]) ).
fof(f6377,plain,
sQ389_spl,
inference(contradiction_clause,[status(thm)],[f6376]) ).
fof(f6884,definition,
( sQ436_spl
<=> leq(host(sK13_skl),zero) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f6885,plain,
( ~ sQ436_spl
| leq(host(sK13_skl),zero) ),
inference(component_clause,[status(thm)],[f6884]) ).
fof(f7169,plain,
( ~ sQ436_spl
| leq(s(zero),zero) ),
inference(resolution,[status(thm)],[f6885,f491]) ).
fof(f7175,plain,
( ~ sQ436_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7169,f191]) ).
fof(f7176,plain,
~ sQ436_spl,
inference(contradiction_clause,[status(thm)],[f7175]) ).
fof(f7220,plain,
( ~ sQ66_spl
| ~ sQ75_spl
| host(sK13_skl) != host(sK13_skl) ),
inference(resolution,[status(thm)],[f1754,f904]) ).
fof(f7221,plain,
( ~ sQ66_spl
| ~ sQ75_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7220]) ).
fof(f7222,plain,
( ~ sQ66_spl
| ~ sQ75_spl ),
inference(contradiction_clause,[status(thm)],[f7221]) ).
fof(f7223,plain,
$false,
inference(sat_refutation,[status(thm)],[f260,f316,f588,f816,f818,f906,f908,f962,f1012,f1042,f1044,f2488,f2499,f2502,f2542,f2681,f2683,f2685,f2710,f2801,f3008,f3012,f3040,f4034,f4072,f4188,f4190,f4319,f5845,f5965,f5968,f6228,f6377,f7176,f7222]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV463+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n016.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 08:57:22 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 5.07/1.18 % Refutation found
% 5.07/1.18 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.07/1.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.07/1.22 % Elapsed time: 0.791446 seconds
% 5.07/1.22 % CPU time: 5.812296 seconds
% 5.07/1.22 % Total memory used: 152.010 MB
% 5.07/1.22 % Net memory used: 145.939 MB
%------------------------------------------------------------------------------