%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV466+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 : n014.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 66.47s 8.98s
% Output : CNFRefutation 66.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 81
% Syntax : Number of formulae : 393 ( 101 unt; 57 def)
% Number of atoms : 1339 ( 410 equ)
% Maximal formula atoms : 92 ( 3 avg)
% Number of connectives : 1600 ( 654 ~; 568 |; 261 &)
% ( 63 <=>; 54 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 63 ( 61 usr; 58 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 21 con; 0-3 aty)
% Number of variables : 464 ( 441 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [P,Q] :
( s(host(P)) = host(Q)
=> host(P) != host(Q) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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(f37,axiom,
! [X,Q] : tail(cons(X,Q)) = Q,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [Y,Q] : init(snoc(Q,Y)) = Q,
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(f44,axiom,
! [X] : cons(X,q_nil) = snoc(q_nil,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X] : ~ elem(X,q_nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X,Y,Q] :
( elem(X,cons(Y,Q))
<=> ( elem(X,Q)
| X = 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(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] :
( ( 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)
=> ( 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)
=> ( ( 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(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] :
( ( 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)
=> ( 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)
=> ( ( 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(V0)
& setIn(V0,alive) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f67]) ).
fof(f72,plain,
! [P,Q] :
( host(P) != host(Q)
| s(host(P)) != host(Q) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f73,plain,
! [X0,X1] :
( host(X0) != host(X1)
| s(host(X0)) != host(X1) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
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(f128,plain,
! [X0,X1] : tail(cons(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f130,plain,
! [X0,X1] : init(snoc(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f39]) ).
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(f135,plain,
! [X0] : cons(X0,q_nil) = snoc(q_nil,X0),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f137,plain,
! [X0] : ~ elem(X0,q_nil),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f138,plain,
! [X,Y,Q] :
( ( ( ~ elem(X,Q)
& X != Y )
| elem(X,cons(Y,Q)) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,cons(Y,Q)) ) ),
inference(NNF_transformation,[status(thm)],[f47]) ).
fof(f139,plain,
( ! [X,Y,Q] :
( ( ~ elem(X,Q)
& X != Y )
| elem(X,cons(Y,Q)) )
& ! [X,Y,Q] :
( elem(X,Q)
| X = Y
| ~ elem(X,cons(Y,Q)) ) ),
inference(miniscoping,[status(thm)],[f138]) ).
fof(f140,plain,
! [X0,X1,X2] :
( elem(X0,X2)
| X0 = X1
| ~ elem(X0,cons(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,plain,
! [X0,X1,X2] :
( X0 != X1
| elem(X0,cons(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
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(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(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(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)
& 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) )
& 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)
| 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,
? [X,Y] :
( ? [Z] :
( ? [V0] :
( ? [Y0] :
( host(X) = 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) )
& 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) )
| ! [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,
( host(sK4_skl) = host(sK9_skl)
& setIn(sK9_skl,alive)
& host(sK11_skl) = s(index(pendack,host(sK10_skl)))
& host(sK12_skl) = index(pendack,host(sK10_skl))
& index(status,host(sK10_skl)) = elec_2
& elem(m_Ack(sK10_skl,sK12_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl)))
& elem(m_Down(sK11_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl)))
& leq(nbr_proc,s(index(pendack,host(sK10_skl))))
& setIn(sK10_skl,alive)
& host(sK4_skl) != host(sK10_skl)
& host(sK8_skl) = host(sK10_skl)
& host(sK4_skl) = host(sK9_skl)
& setIn(host(sK8_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),sK7_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)))
| ( sK6_skl(Pid20,Pid0,Pid30) != host(Pid20)
& ~ setIn(sK6_skl(Pid20,Pid0,Pid30),index(down,host(Pid0)))
& leq(s(zero),sK6_skl(Pid20,Pid0,Pid30))
& ~ leq(host(Pid0),sK6_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]),skolemize(X,sK4_skl),skolemize(Y,sK5_skl),skolemize(V0,sK6_skl(Pid20,Pid0,Pid30)),skolemize(V,sK7_skl),skolemize(Z,sK8_skl),skolemize(V0,sK9_skl),skolemize(Y0,sK10_skl),skolemize(X0,sK11_skl),skolemize(W0,sK12_skl)],[f213]) ).
fof(f216,plain,
! [X0,X1] :
( host(X0) != host(X1)
| ~ elem(m_Down(X0),queue(host(X1))) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f219,plain,
! [X0,X1] :
( ~ setIn(X0,alive)
| ~ setIn(X1,alive)
| host(X0) != host(X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f223,plain,
! [X0] :
( index(elid,host(X0)) = X0
| ~ setIn(X0,alive)
| index(status,host(X0)) != elec_2 ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f225,plain,
! [X0,X1] :
( leq(index(pendack,host(X1)),host(X0))
| index(status,host(X1)) != elec_2
| index(status,host(X0)) != elec_2
| ~ setIn(X1,alive)
| ~ setIn(X0,alive)
| leq(host(X0),host(X1)) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f226,plain,
! [X0,X1,X2] :
( ~ elem(m_Ack(X0,X2),queue(host(X0)))
| index(status,host(X1)) != elec_2
| index(status,host(X0)) != elec_2
| host(X1) != host(X2)
| ~ setIn(X1,alive)
| ~ setIn(X0,alive) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f227,plain,
! [X0,X1] :
( ~ leq(index(pendack,host(X0)),index(pendack,host(X1)))
| index(status,host(X1)) != elec_2
| index(status,host(X0)) != elec_2
| ~ setIn(X1,alive)
| ~ setIn(X0,alive)
| leq(host(X0),host(X1)) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f234,plain,
queue(host(sK4_skl)) = cons(m_Down(sK5_skl),sK7_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f235,plain,
setIn(sK4_skl,alive),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f236,plain,
leq(host(sK4_skl),host(sK5_skl)),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f237,plain,
index(status,host(sK4_skl)) = elec_2,
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f238,plain,
host(sK5_skl) = index(pendack,host(sK4_skl)),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f239,plain,
leq(nbr_proc,index(pendack,host(sK4_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f241,plain,
host(sK4_skl) = host(sK9_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f242,plain,
host(sK8_skl) = host(sK10_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f243,plain,
host(sK4_skl) != host(sK10_skl),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f244,plain,
setIn(sK10_skl,alive),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f245,plain,
leq(nbr_proc,s(index(pendack,host(sK10_skl)))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f247,plain,
elem(m_Ack(sK10_skl,sK12_skl),snoc(queue(host(sK10_skl)),m_Ldr(sK4_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f248,plain,
index(status,host(sK10_skl)) = elec_2,
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f249,plain,
host(sK12_skl) = index(pendack,host(sK10_skl)),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f250,plain,
host(sK11_skl) = s(index(pendack,host(sK10_skl))),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f251,plain,
setIn(sK9_skl,alive),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f260,plain,
! [X0,X1] : elem(X0,cons(X0,X1)),
inference(destructive_equality_resolution,[status(thm)],[f141]) ).
fof(f263,plain,
! [X0] : pidElem(m_Down(X0)),
inference(destructive_equality_resolution,[status(thm)],[f153]) ).
fof(f311,plain,
! [X0] :
( ~ setIn(X0,alive)
| host(X0) != host(sK10_skl)
| X0 = sK10_skl ),
inference(resolution,[status(thm)],[f219,f244]) ).
fof(f313,plain,
! [X0] :
( ~ setIn(X0,alive)
| host(X0) != host(sK8_skl)
| X0 = sK10_skl ),
inference(forward_demodulation,[status(thm)],[f242,f311]) ).
fof(f319,plain,
host(sK9_skl) != host(sK10_skl),
inference(forward_demodulation,[status(thm)],[f241,f243]) ).
fof(f320,plain,
host(sK9_skl) != host(sK8_skl),
inference(forward_demodulation,[status(thm)],[f242,f319]) ).
fof(f323,definition,
( sQ6_spl
<=> setIn(sK10_skl,alive) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f325,plain,
( sQ6_spl
| ~ setIn(sK10_skl,alive) ),
inference(component_clause,[status(thm)],[f323]) ).
fof(f339,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f325,f244]) ).
fof(f340,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f339]) ).
fof(f389,plain,
! [X0] : init(cons(X0,q_nil)) = q_nil,
inference(paramodulation,[status(thm)],[f135,f130]) ).
fof(f405,plain,
leq(host(sK9_skl),host(sK5_skl)),
inference(forward_demodulation,[status(thm)],[f241,f236]) ).
fof(f412,definition,
( sQ15_spl
<=> index(elid,host(sK9_skl)) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( ~ sQ15_spl
| index(elid,host(sK9_skl)) = sK9_skl ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f420,definition,
( sQ17_spl
<=> index(elid,host(sK4_skl)) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( ~ sQ17_spl
| index(elid,host(sK4_skl)) = sK4_skl ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f455,plain,
( host(sK9_skl) = host(sK5_skl)
| ~ leq(host(sK5_skl),host(sK9_skl)) ),
inference(resolution,[status(thm)],[f196,f405]) ).
fof(f465,definition,
( sQ18_spl
<=> leq(host(sK5_skl),host(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( sQ18_spl
| ~ leq(host(sK5_skl),host(sK9_skl)) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f468,definition,
( sQ19_spl
<=> host(sK9_skl) = host(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ19_spl
| host(sK9_skl) = host(sK5_skl) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,plain,
( sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f455,f465,f468]) ).
fof(f487,plain,
index(status,host(sK9_skl)) = elec_2,
inference(forward_demodulation,[status(thm)],[f241,f237]) ).
fof(f488,plain,
( index(elid,host(sK9_skl)) = sK9_skl
| index(status,host(sK9_skl)) != elec_2 ),
inference(resolution,[status(thm)],[f223,f251]) ).
fof(f490,plain,
( index(elid,host(sK4_skl)) = sK4_skl
| index(status,host(sK4_skl)) != elec_2 ),
inference(resolution,[status(thm)],[f223,f235]) ).
fof(f491,definition,
( sQ22_spl
<=> index(status,host(sK9_skl)) = elec_2 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ22_spl
| index(status,host(sK9_skl)) != elec_2 ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,plain,
( sQ15_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f488,f491,f412]) ).
fof(f495,definition,
( sQ23_spl
<=> index(status,host(sK10_skl)) = elec_2 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( sQ23_spl
| index(status,host(sK10_skl)) != elec_2 ),
inference(component_clause,[status(thm)],[f495]) ).
fof(f499,definition,
( sQ24_spl
<=> index(status,host(sK4_skl)) = elec_2 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( sQ24_spl
| index(status,host(sK4_skl)) != elec_2 ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,plain,
( sQ17_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f490,f499,f420]) ).
fof(f503,plain,
( ~ sQ17_spl
| index(elid,host(sK9_skl)) = sK4_skl ),
inference(forward_demodulation,[status(thm)],[f241,f421]) ).
fof(f509,plain,
leq(s(zero),s(nbr_proc)),
inference(resolution,[status(thm)],[f210,f75]) ).
fof(f510,plain,
! [X0] : leq(s(zero),s(host(X0))),
inference(resolution,[status(thm)],[f210,f74]) ).
fof(f524,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| leq(X2,X1)
| ~ leq(X0,X1) ),
inference(resolution,[status(thm)],[f201,f193]) ).
fof(f536,plain,
index(status,host(sK8_skl)) = elec_2,
inference(forward_demodulation,[status(thm)],[f242,f248]) ).
fof(f616,plain,
! [X0] :
( leq(index(pendack,host(X0)),host(sK4_skl))
| index(status,host(X0)) != elec_2
| index(status,host(sK4_skl)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK4_skl),host(X0)) ),
inference(resolution,[status(thm)],[f225,f235]) ).
fof(f625,definition,
! [X0] :
( sQ29_spl
<=> ( leq(index(pendack,host(X0)),host(sK4_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK4_skl),host(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f626,plain,
! [X0] :
( ~ sQ29_spl
| leq(index(pendack,host(X0)),host(sK4_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK4_skl),host(X0)) ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f628,plain,
( ~ sQ24_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f616,f625,f499]) ).
fof(f629,plain,
( sQ24_spl
| index(status,host(sK9_skl)) != elec_2 ),
inference(forward_demodulation,[status(thm)],[f241,f501]) ).
fof(f630,plain,
( sQ24_spl
| elec_2 != elec_2 ),
inference(forward_demodulation,[status(thm)],[f487,f629]) ).
fof(f631,plain,
( sQ24_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f630]) ).
fof(f632,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f631]) ).
fof(f633,plain,
( sQ23_spl
| index(status,host(sK8_skl)) != elec_2 ),
inference(forward_demodulation,[status(thm)],[f242,f497]) ).
fof(f634,plain,
( sQ23_spl
| elec_2 != elec_2 ),
inference(forward_demodulation,[status(thm)],[f536,f633]) ).
fof(f635,plain,
( sQ23_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f634]) ).
fof(f636,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f635]) ).
fof(f637,plain,
( sQ22_spl
| elec_2 != elec_2 ),
inference(forward_demodulation,[status(thm)],[f487,f493]) ).
fof(f638,plain,
( sQ22_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f637]) ).
fof(f639,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f638]) ).
fof(f640,plain,
! [X0] :
( ~ sQ29_spl
| leq(index(pendack,host(X0)),host(sK4_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK9_skl),host(X0)) ),
inference(forward_demodulation,[status(thm)],[f241,f626]) ).
fof(f641,plain,
! [X0] :
( ~ sQ29_spl
| leq(index(pendack,host(X0)),host(sK9_skl))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK9_skl),host(X0)) ),
inference(forward_demodulation,[status(thm)],[f241,f640]) ).
fof(f673,plain,
! [X0,X1] :
( ~ elem(m_Ack(X0,X1),queue(host(X0)))
| index(status,host(sK4_skl)) != elec_2
| index(status,host(X0)) != elec_2
| host(sK4_skl) != host(X1)
| ~ setIn(X0,alive) ),
inference(resolution,[status(thm)],[f226,f235]) ).
fof(f682,definition,
! [X0,X1] :
( sQ32_spl
<=> ( ~ elem(m_Ack(X0,X1),queue(host(X0)))
| index(status,host(X0)) != elec_2
| host(sK4_skl) != host(X1)
| ~ setIn(X0,alive) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f683,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ elem(m_Ack(X0,X1),queue(host(X0)))
| index(status,host(X0)) != elec_2
| host(sK4_skl) != host(X1)
| ~ setIn(X0,alive) ),
inference(component_clause,[status(thm)],[f682]) ).
fof(f685,plain,
( ~ sQ24_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f673,f682,f499]) ).
fof(f686,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ elem(m_Ack(X0,X1),queue(host(X0)))
| index(status,host(X0)) != elec_2
| host(sK9_skl) != host(X1)
| ~ setIn(X0,alive) ),
inference(forward_demodulation,[status(thm)],[f241,f683]) ).
fof(f709,plain,
! [X0] :
( ~ leq(index(pendack,host(sK8_skl)),index(pendack,host(X0)))
| index(status,host(X0)) != elec_2
| index(status,host(sK10_skl)) != elec_2
| ~ setIn(X0,alive)
| ~ setIn(sK10_skl,alive)
| leq(host(sK10_skl),host(X0)) ),
inference(paramodulation,[status(thm)],[f242,f227]) ).
fof(f716,definition,
! [X0] :
( sQ33_spl
<=> ( ~ leq(index(pendack,host(sK8_skl)),index(pendack,host(X0)))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK10_skl),host(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f717,plain,
! [X0] :
( ~ sQ33_spl
| ~ leq(index(pendack,host(sK8_skl)),index(pendack,host(X0)))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK10_skl),host(X0)) ),
inference(component_clause,[status(thm)],[f716]) ).
fof(f719,plain,
( ~ sQ23_spl
| ~ sQ6_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f709,f716,f323,f495]) ).
fof(f734,plain,
! [X0] :
( ~ sQ33_spl
| ~ leq(index(pendack,host(sK8_skl)),index(pendack,host(X0)))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK8_skl),host(X0)) ),
inference(forward_demodulation,[status(thm)],[f242,f717]) ).
fof(f772,plain,
leq(zero,nbr_proc),
inference(resolution,[status(thm)],[f509,f205]) ).
fof(f815,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| sK9_skl = sK4_skl ),
inference(forward_demodulation,[status(thm)],[f413,f503]) ).
fof(f822,plain,
! [X0] :
( leq(zero,X0)
| ~ leq(nbr_proc,X0) ),
inference(resolution,[status(thm)],[f772,f201]) ).
fof(f834,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| queue(host(sK9_skl)) = cons(m_Down(sK5_skl),sK7_skl) ),
inference(forward_demodulation,[status(thm)],[f815,f234]) ).
fof(f858,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| host(sK5_skl) = index(pendack,host(sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f815,f238]) ).
fof(f864,definition,
( sQ56_spl
<=> setIn(sK9_skl,alive) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f866,plain,
( sQ56_spl
| ~ setIn(sK9_skl,alive) ),
inference(component_clause,[status(thm)],[f864]) ).
fof(f872,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f866,f251]) ).
fof(f873,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f872]) ).
fof(f901,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| leq(nbr_proc,index(pendack,host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f815,f239]) ).
fof(f902,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| leq(nbr_proc,host(sK5_skl)) ),
inference(forward_demodulation,[status(thm)],[f858,f901]) ).
fof(f904,plain,
leq(nbr_proc,s(index(pendack,host(sK8_skl)))),
inference(forward_demodulation,[status(thm)],[f242,f245]) ).
fof(f947,definition,
( sQ64_spl
<=> leq(zero,nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f967,plain,
elem(m_Ack(sK10_skl,sK12_skl),snoc(queue(host(sK8_skl)),m_Ldr(sK4_skl))),
inference(forward_demodulation,[status(thm)],[f242,f247]) ).
fof(f968,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| elem(m_Ack(sK10_skl,sK12_skl),snoc(queue(host(sK8_skl)),m_Ldr(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f815,f967]) ).
fof(f969,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| elem(m_Ack(sK10_skl,sK12_skl),queue(host(sK8_skl)))
| m_Ack(sK10_skl,sK12_skl) = m_Ldr(sK9_skl) ),
inference(resolution,[status(thm)],[f968,f145]) ).
fof(f972,definition,
( sQ66_spl
<=> m_Ack(sK10_skl,sK12_skl) = m_Ldr(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f973,plain,
( ~ sQ66_spl
| m_Ack(sK10_skl,sK12_skl) = m_Ldr(sK9_skl) ),
inference(component_clause,[status(thm)],[f972]) ).
fof(f975,definition,
( sQ67_spl
<=> elem(m_Ack(sK10_skl,sK12_skl),queue(host(sK8_skl))) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f976,plain,
( ~ sQ67_spl
| elem(m_Ack(sK10_skl,sK12_skl),queue(host(sK8_skl))) ),
inference(component_clause,[status(thm)],[f975]) ).
fof(f978,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| sQ67_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f969,f972,f975,f412,f420]) ).
fof(f979,plain,
( ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f973,f86]) ).
fof(f980,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f979]) ).
fof(f981,plain,
leq(nbr_proc,s(host(sK12_skl))),
inference(backward_demodulation,[status(thm)],[f982,f904]) ).
fof(f982,plain,
host(sK12_skl) = index(pendack,host(sK8_skl)),
inference(forward_demodulation,[status(thm)],[f242,f249]) ).
fof(f1006,plain,
host(sK11_skl) = s(index(pendack,host(sK8_skl))),
inference(forward_demodulation,[status(thm)],[f242,f250]) ).
fof(f1007,plain,
host(sK11_skl) = s(host(sK12_skl)),
inference(forward_demodulation,[status(thm)],[f982,f1006]) ).
fof(f1011,plain,
! [X0] :
( ~ leq(s(X0),host(sK11_skl))
| leq(X0,host(sK12_skl)) ),
inference(paramodulation,[status(thm)],[f1007,f205]) ).
fof(f1034,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| nbr_proc = host(sK5_skl)
| ~ leq(host(sK5_skl),nbr_proc) ),
inference(resolution,[status(thm)],[f902,f196]) ).
fof(f1035,definition,
( sQ75_spl
<=> leq(host(sK5_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( sQ75_spl
| ~ leq(host(sK5_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f1035]) ).
fof(f1038,definition,
( sQ76_spl
<=> nbr_proc = host(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1039,plain,
( ~ sQ76_spl
| nbr_proc = host(sK5_skl) ),
inference(component_clause,[status(thm)],[f1038]) ).
fof(f1041,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| sQ76_spl
| ~ sQ75_spl ),
inference(split_clause,[status(thm)],[f1034,f1035,f1038,f412,f420]) ).
fof(f1042,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1037,f76]) ).
fof(f1043,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1042]) ).
fof(f1047,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| ~ sQ76_spl
| nbr_proc = index(pendack,host(sK9_skl)) ),
inference(backward_demodulation,[status(thm)],[f1039,f858]) ).
fof(f1048,plain,
( sQ18_spl
| ~ sQ76_spl
| ~ leq(nbr_proc,host(sK9_skl)) ),
inference(backward_demodulation,[status(thm)],[f1039,f467]) ).
fof(f1063,plain,
! [X0] :
( ~ sQ76_spl
| host(X0) != host(sK5_skl)
| ~ elem(m_Down(X0),queue(nbr_proc)) ),
inference(paramodulation,[status(thm)],[f1039,f216]) ).
fof(f1114,plain,
! [X0] :
( ~ sQ76_spl
| host(X0) != nbr_proc
| ~ elem(m_Down(X0),queue(nbr_proc)) ),
inference(forward_demodulation,[status(thm)],[f1039,f1063]) ).
fof(f1143,plain,
leq(nbr_proc,host(sK11_skl)),
inference(forward_demodulation,[status(thm)],[f1007,f981]) ).
fof(f1147,plain,
( nbr_proc = host(sK11_skl)
| ~ leq(host(sK11_skl),nbr_proc) ),
inference(resolution,[status(thm)],[f1143,f196]) ).
fof(f1148,definition,
( sQ90_spl
<=> leq(host(sK11_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( sQ90_spl
| ~ leq(host(sK11_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f1148]) ).
fof(f1151,definition,
( sQ91_spl
<=> nbr_proc = host(sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1152,plain,
( ~ sQ91_spl
| nbr_proc = host(sK11_skl) ),
inference(component_clause,[status(thm)],[f1151]) ).
fof(f1154,plain,
( sQ91_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f1147,f1148,f1151]) ).
fof(f1155,plain,
( sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1150,f76]) ).
fof(f1156,plain,
sQ90_spl,
inference(contradiction_clause,[status(thm)],[f1155]) ).
fof(f1189,plain,
( ~ sQ91_spl
| nbr_proc = s(host(sK12_skl)) ),
inference(backward_demodulation,[status(thm)],[f1152,f1007]) ).
fof(f1295,definition,
( sQ112_spl
<=> sK10_skl = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1296,plain,
( ~ sQ112_spl
| sK10_skl = sK9_skl ),
inference(component_clause,[status(thm)],[f1295]) ).
fof(f1307,plain,
( ~ sQ112_spl
| host(sK8_skl) = host(sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f1296,f242]) ).
fof(f1309,plain,
( ~ sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1307,f320]) ).
fof(f1310,plain,
~ sQ112_spl,
inference(contradiction_clause,[status(thm)],[f1309]) ).
fof(f1359,plain,
( host(sK9_skl) != host(sK8_skl)
| sK9_skl = sK10_skl ),
inference(resolution,[status(thm)],[f313,f251]) ).
fof(f1367,definition,
( sQ116_spl
<=> host(sK9_skl) = host(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1370,plain,
( ~ sQ116_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1359,f1295,f1367]) ).
fof(f1558,plain,
( ~ sQ19_spl
| ~ sQ76_spl
| host(sK9_skl) = nbr_proc ),
inference(forward_demodulation,[status(thm)],[f1039,f469]) ).
fof(f1837,definition,
( sQ159_spl
<=> leq(nbr_proc,nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1839,plain,
( sQ159_spl
| ~ leq(nbr_proc,nbr_proc) ),
inference(component_clause,[status(thm)],[f1837]) ).
fof(f2147,plain,
! [X0] : leq(zero,host(X0)),
inference(resolution,[status(thm)],[f510,f205]) ).
fof(f2347,plain,
( ~ sQ29_spl
| leq(index(pendack,host(sK10_skl)),host(sK9_skl))
| index(status,host(sK10_skl)) != elec_2
| leq(host(sK9_skl),host(sK10_skl)) ),
inference(resolution,[status(thm)],[f641,f244]) ).
fof(f2349,definition,
( sQ173_spl
<=> leq(host(sK9_skl),host(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f2350,plain,
( ~ sQ173_spl
| leq(host(sK9_skl),host(sK10_skl)) ),
inference(component_clause,[status(thm)],[f2349]) ).
fof(f2352,definition,
( sQ174_spl
<=> leq(index(pendack,host(sK10_skl)),host(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f2353,plain,
( ~ sQ174_spl
| leq(index(pendack,host(sK10_skl)),host(sK9_skl)) ),
inference(component_clause,[status(thm)],[f2352]) ).
fof(f2355,plain,
( ~ sQ29_spl
| sQ174_spl
| ~ sQ23_spl
| sQ173_spl ),
inference(split_clause,[status(thm)],[f2347,f2349,f495,f2352,f625]) ).
fof(f2363,plain,
( ~ sQ173_spl
| leq(host(sK9_skl),host(sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f242,f2350]) ).
fof(f2365,plain,
( ~ sQ174_spl
| leq(index(pendack,host(sK8_skl)),host(sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f242,f2353]) ).
fof(f2366,plain,
( ~ sQ174_spl
| leq(host(sK12_skl),host(sK9_skl)) ),
inference(forward_demodulation,[status(thm)],[f982,f2365]) ).
fof(f2384,plain,
! [X0,X1] :
( leq(zero,X1)
| ~ leq(host(X0),X1) ),
inference(resolution,[status(thm)],[f2147,f201]) ).
fof(f2422,plain,
! [X0,X1] :
( leq(zero,X0)
| leq(X0,host(X1)) ),
inference(resolution,[status(thm)],[f524,f2147]) ).
fof(f2423,plain,
! [X0] :
( leq(zero,X0)
| leq(X0,nbr_proc) ),
inference(resolution,[status(thm)],[f524,f772]) ).
fof(f2471,definition,
! [X0] :
( sQ179_spl
<=> pidElem(X0) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f2472,plain,
! [X0] :
( ~ sQ179_spl
| pidElem(X0) ),
inference(component_clause,[status(thm)],[f2471]) ).
fof(f2652,plain,
! [X0] :
( ~ sQ179_spl
| X0 = m_Down(sK1_skl(X0))
| X0 = m_Halt(sK0_skl(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f151,f2472]) ).
fof(f2819,definition,
( sQ199_spl
<=> leq(host(sK8_skl),host(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f2907,plain,
! [X0] :
( ~ sQ32_spl
| ~ elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl)))
| index(status,host(sK10_skl)) != elec_2
| host(sK9_skl) != host(X0)
| ~ setIn(sK10_skl,alive) ),
inference(paramodulation,[status(thm)],[f242,f686]) ).
fof(f2910,definition,
! [X0] :
( sQ203_spl
<=> ( ~ elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl)))
| host(sK9_skl) != host(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f2911,plain,
! [X0] :
( ~ sQ203_spl
| ~ elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl)))
| host(sK9_skl) != host(X0) ),
inference(component_clause,[status(thm)],[f2910]) ).
fof(f2913,plain,
( ~ sQ32_spl
| ~ sQ23_spl
| sQ203_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2907,f323,f2910,f495,f682]) ).
fof(f3137,plain,
( sQ159_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1839,f192]) ).
fof(f3138,plain,
sQ159_spl,
inference(contradiction_clause,[status(thm)],[f3137]) ).
fof(f3152,definition,
( sQ216_spl
<=> leq(host(sK12_skl),nbr_proc) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f3154,plain,
( sQ216_spl
| ~ leq(host(sK12_skl),nbr_proc) ),
inference(component_clause,[status(thm)],[f3152]) ).
fof(f3179,plain,
( sQ216_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3154,f76]) ).
fof(f3180,plain,
sQ216_spl,
inference(contradiction_clause,[status(thm)],[f3179]) ).
fof(f3199,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ76_spl
| queue(nbr_proc) = cons(m_Down(sK5_skl),sK7_skl) ),
inference(backward_demodulation,[status(thm)],[f1558,f834]) ).
fof(f3254,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ76_spl
| elem(m_Down(sK5_skl),queue(nbr_proc)) ),
inference(paramodulation,[status(thm)],[f3199,f260]) ).
fof(f3293,plain,
! [X0] :
( ~ sQ33_spl
| ~ leq(host(sK12_skl),index(pendack,host(X0)))
| index(status,host(X0)) != elec_2
| ~ setIn(X0,alive)
| leq(host(sK8_skl),host(X0)) ),
inference(forward_demodulation,[status(thm)],[f982,f734]) ).
fof(f3472,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| ~ sQ76_spl
| ~ sQ33_spl
| ~ leq(host(sK12_skl),nbr_proc)
| index(status,host(sK9_skl)) != elec_2
| ~ setIn(sK9_skl,alive)
| leq(host(sK8_skl),host(sK9_skl)) ),
inference(paramodulation,[status(thm)],[f1047,f3293]) ).
fof(f3476,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| ~ sQ76_spl
| ~ sQ33_spl
| ~ sQ216_spl
| ~ sQ22_spl
| ~ sQ56_spl
| sQ199_spl ),
inference(split_clause,[status(thm)],[f3472,f2819,f864,f491,f3152,f716,f1038,f412,f420]) ).
fof(f3784,plain,
! [X0] :
( ~ sQ91_spl
| ~ leq(s(X0),nbr_proc)
| leq(X0,host(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f1152,f1011]) ).
fof(f3996,plain,
( ~ sQ173_spl
| host(sK9_skl) = host(sK8_skl)
| ~ leq(host(sK8_skl),host(sK9_skl)) ),
inference(resolution,[status(thm)],[f2363,f196]) ).
fof(f3997,plain,
( ~ sQ173_spl
| sQ116_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f3996,f2819,f1367,f2349]) ).
fof(f4001,plain,
( ~ sQ174_spl
| leq(s(host(sK12_skl)),s(host(sK9_skl))) ),
inference(resolution,[status(thm)],[f2366,f204]) ).
fof(f4004,plain,
( ~ sQ174_spl
| host(sK12_skl) = host(sK9_skl)
| ~ leq(host(sK9_skl),host(sK12_skl)) ),
inference(resolution,[status(thm)],[f2366,f196]) ).
fof(f4005,plain,
( ~ sQ174_spl
| ~ sQ91_spl
| leq(nbr_proc,s(host(sK9_skl))) ),
inference(forward_demodulation,[status(thm)],[f1189,f4001]) ).
fof(f4006,definition,
( sQ278_spl
<=> leq(host(sK9_skl),host(sK12_skl)) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f4009,definition,
( sQ279_spl
<=> host(sK12_skl) = host(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f4010,plain,
( ~ sQ279_spl
| host(sK12_skl) = host(sK9_skl) ),
inference(component_clause,[status(thm)],[f4009]) ).
fof(f4012,plain,
( ~ sQ174_spl
| sQ279_spl
| ~ sQ278_spl ),
inference(split_clause,[status(thm)],[f4004,f4006,f4009,f2352]) ).
fof(f4076,definition,
( sQ282_spl
<=> host(sK12_skl) = host(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f4078,plain,
( sQ282_spl
| host(sK12_skl) != host(sK12_skl) ),
inference(component_clause,[status(thm)],[f4076]) ).
fof(f4149,plain,
( sQ282_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4078]) ).
fof(f4150,plain,
sQ282_spl,
inference(contradiction_clause,[status(thm)],[f4149]) ).
fof(f4243,definition,
( sQ302_spl
<=> leq(s(zero),s(zero)) ),
introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition]) ).
fof(f4245,plain,
( sQ302_spl
| ~ leq(s(zero),s(zero)) ),
inference(component_clause,[status(thm)],[f4243]) ).
fof(f4304,plain,
( sQ302_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4245,f192]) ).
fof(f4305,plain,
sQ302_spl,
inference(contradiction_clause,[status(thm)],[f4304]) ).
fof(f4475,plain,
( leq(zero,nbr_proc)
| leq(zero,nbr_proc) ),
inference(resolution,[status(thm)],[f2423,f822]) ).
fof(f4496,plain,
sQ64_spl,
inference(split_clause,[status(thm)],[f4475,f947]) ).
fof(f4502,definition,
! [X0] :
( sQ330_spl
<=> leq(zero,host(X0)) ),
introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition]) ).
fof(f4526,definition,
( sQ332_spl
<=> leq(s(zero),index(pendack,host(sK8_skl))) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f4528,plain,
( sQ332_spl
| ~ leq(s(zero),index(pendack,host(sK8_skl))) ),
inference(component_clause,[status(thm)],[f4526]) ).
fof(f7344,plain,
( sQ332_spl
| ~ leq(s(zero),host(sK12_skl)) ),
inference(forward_demodulation,[status(thm)],[f982,f4528]) ).
fof(f7345,plain,
( sQ332_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7344,f74]) ).
fof(f7346,plain,
sQ332_spl,
inference(contradiction_clause,[status(thm)],[f7345]) ).
fof(f7514,definition,
( sQ456_spl
<=> elem(m_Down(sK5_skl),queue(nbr_proc)) ),
introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition]) ).
fof(f7515,plain,
( ~ sQ456_spl
| elem(m_Down(sK5_skl),queue(nbr_proc)) ),
inference(component_clause,[status(thm)],[f7514]) ).
fof(f8933,definition,
( sQ506_spl
<=> host(pidMsg(last(sK7_skl))) = host(pidMsg(last(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition]) ).
fof(f8935,plain,
( sQ506_spl
| host(pidMsg(last(sK7_skl))) != host(pidMsg(last(sK7_skl))) ),
inference(component_clause,[status(thm)],[f8933]) ).
fof(f8948,plain,
( sQ506_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8935]) ).
fof(f8949,plain,
sQ506_spl,
inference(contradiction_clause,[status(thm)],[f8948]) ).
fof(f10450,definition,
! [X0,X1] :
( sQ580_spl
<=> elem(X0,cons(X1,q_nil)) ),
introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition]) ).
fof(f10451,plain,
! [X0,X1] :
( ~ sQ580_spl
| elem(X0,cons(X1,q_nil)) ),
inference(component_clause,[status(thm)],[f10450]) ).
fof(f10458,definition,
! [X0] :
( sQ582_spl
<=> elem(X0,q_nil) ),
introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition]) ).
fof(f10459,plain,
! [X0] :
( ~ sQ582_spl
| elem(X0,q_nil) ),
inference(component_clause,[status(thm)],[f10458]) ).
fof(f10462,definition,
! [X0] :
( sQ583_spl
<=> q_nil = snoc(init(q_nil),X0) ),
introduced(definition,[new_symbols(definition,[sQ583_spl])],[split_symbol_definition]) ).
fof(f10463,plain,
! [X0] :
( ~ sQ583_spl
| q_nil = snoc(init(q_nil),X0) ),
inference(component_clause,[status(thm)],[f10462]) ).
fof(f10466,plain,
( ~ sQ583_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10463,f134]) ).
fof(f10467,plain,
~ sQ583_spl,
inference(contradiction_clause,[status(thm)],[f10466]) ).
fof(f10468,plain,
( ~ sQ582_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10459,f137]) ).
fof(f10469,plain,
~ sQ582_spl,
inference(contradiction_clause,[status(thm)],[f10468]) ).
fof(f11083,plain,
! [X0,X1] :
( ~ sQ580_spl
| elem(X0,q_nil)
| X0 = X1 ),
inference(resolution,[status(thm)],[f10451,f140]) ).
fof(f11086,plain,
! [X0,X1] :
( ~ sQ580_spl
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f11083,f137]) ).
fof(f11095,plain,
! [X0,X1] :
( ~ sQ580_spl
| s(host(X0)) != host(X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f73,f11086]) ).
fof(f11146,plain,
( ~ sQ580_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11095,f11086]) ).
fof(f11147,plain,
~ sQ580_spl,
inference(contradiction_clause,[status(thm)],[f11146]) ).
fof(f12545,definition,
( sQ600_spl
<=> host(pidMsg(head(sK7_skl))) = host(pidMsg(head(sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ600_spl])],[split_symbol_definition]) ).
fof(f12547,plain,
( sQ600_spl
| host(pidMsg(head(sK7_skl))) != host(pidMsg(head(sK7_skl))) ),
inference(component_clause,[status(thm)],[f12545]) ).
fof(f12566,plain,
( sQ600_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f12547]) ).
fof(f12567,plain,
sQ600_spl,
inference(contradiction_clause,[status(thm)],[f12566]) ).
fof(f13030,definition,
( sQ654_spl
<=> cons(head(sK7_skl),sK7_skl) = q_nil ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f13031,plain,
( ~ sQ654_spl
| cons(head(sK7_skl),sK7_skl) = q_nil ),
inference(component_clause,[status(thm)],[f13030]) ).
fof(f13045,plain,
( ~ sQ654_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13031,f133]) ).
fof(f13046,plain,
~ sQ654_spl,
inference(contradiction_clause,[status(thm)],[f13045]) ).
fof(f13229,plain,
( ~ sQ456_spl
| ~ sQ76_spl
| host(sK5_skl) != nbr_proc ),
inference(resolution,[status(thm)],[f1114,f7515]) ).
fof(f13230,plain,
( ~ sQ456_spl
| ~ sQ76_spl
| nbr_proc != nbr_proc ),
inference(forward_demodulation,[status(thm)],[f1039,f13229]) ).
fof(f13231,plain,
( ~ sQ456_spl
| ~ sQ76_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f13230]) ).
fof(f13232,plain,
( ~ sQ456_spl
| ~ sQ76_spl ),
inference(contradiction_clause,[status(thm)],[f13231]) ).
fof(f13314,definition,
( sQ671_spl
<=> s(zero) = s(s(nbr_proc)) ),
introduced(definition,[new_symbols(definition,[sQ671_spl])],[split_symbol_definition]) ).
fof(f13315,plain,
( ~ sQ671_spl
| s(zero) = s(s(nbr_proc)) ),
inference(component_clause,[status(thm)],[f13314]) ).
fof(f13794,definition,
( sQ694_spl
<=> pidElem(m_Down(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ694_spl])],[split_symbol_definition]) ).
fof(f13796,plain,
( sQ694_spl
| ~ pidElem(m_Down(sK11_skl)) ),
inference(component_clause,[status(thm)],[f13794]) ).
fof(f13824,plain,
( sQ694_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13796,f263]) ).
fof(f13825,plain,
sQ694_spl,
inference(contradiction_clause,[status(thm)],[f13824]) ).
fof(f13843,definition,
! [X0] :
( sQ702_spl
<=> init(cons(X0,q_nil)) = cons(X0,q_nil) ),
introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition]) ).
fof(f13844,plain,
! [X0] :
( ~ sQ702_spl
| init(cons(X0,q_nil)) = cons(X0,q_nil) ),
inference(component_clause,[status(thm)],[f13843]) ).
fof(f13849,plain,
! [X0] :
( ~ sQ702_spl
| q_nil = cons(X0,q_nil) ),
inference(forward_demodulation,[status(thm)],[f389,f13844]) ).
fof(f13850,plain,
( ~ sQ702_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13849,f133]) ).
fof(f13851,plain,
~ sQ702_spl,
inference(contradiction_clause,[status(thm)],[f13850]) ).
fof(f13893,definition,
( sQ705_spl
<=> elem(last(q_nil),q_nil) ),
introduced(definition,[new_symbols(definition,[sQ705_spl])],[split_symbol_definition]) ).
fof(f13894,plain,
( ~ sQ705_spl
| elem(last(q_nil),q_nil) ),
inference(component_clause,[status(thm)],[f13893]) ).
fof(f13905,plain,
( ~ sQ705_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13894,f137]) ).
fof(f13906,plain,
~ sQ705_spl,
inference(contradiction_clause,[status(thm)],[f13905]) ).
fof(f14222,definition,
( sQ731_spl
<=> elem(head(q_nil),q_nil) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f14223,plain,
( ~ sQ731_spl
| elem(head(q_nil),q_nil) ),
inference(component_clause,[status(thm)],[f14222]) ).
fof(f14226,definition,
( sQ732_spl
<=> q_nil = snoc(init(q_nil),head(q_nil)) ),
introduced(definition,[new_symbols(definition,[sQ732_spl])],[split_symbol_definition]) ).
fof(f14227,plain,
( ~ sQ732_spl
| q_nil = snoc(init(q_nil),head(q_nil)) ),
inference(component_clause,[status(thm)],[f14226]) ).
fof(f14234,plain,
( ~ sQ731_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14223,f137]) ).
fof(f14235,plain,
~ sQ731_spl,
inference(contradiction_clause,[status(thm)],[f14234]) ).
fof(f14348,definition,
! [X0] :
( sQ740_spl
<=> q_nil = cons(X0,tail(q_nil)) ),
introduced(definition,[new_symbols(definition,[sQ740_spl])],[split_symbol_definition]) ).
fof(f14349,plain,
! [X0] :
( ~ sQ740_spl
| q_nil = cons(X0,tail(q_nil)) ),
inference(component_clause,[status(thm)],[f14348]) ).
fof(f14352,plain,
( ~ sQ740_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14349,f133]) ).
fof(f14353,plain,
~ sQ740_spl,
inference(contradiction_clause,[status(thm)],[f14352]) ).
fof(f14625,definition,
! [X0] :
( sQ756_spl
<=> tail(snoc(q_nil,X0)) = snoc(q_nil,X0) ),
introduced(definition,[new_symbols(definition,[sQ756_spl])],[split_symbol_definition]) ).
fof(f14626,plain,
! [X0] :
( ~ sQ756_spl
| tail(snoc(q_nil,X0)) = snoc(q_nil,X0) ),
inference(component_clause,[status(thm)],[f14625]) ).
fof(f14640,plain,
! [X0] :
( ~ sQ756_spl
| tail(cons(X0,q_nil)) = snoc(q_nil,X0) ),
inference(forward_demodulation,[status(thm)],[f135,f14626]) ).
fof(f14641,plain,
! [X0] :
( ~ sQ756_spl
| q_nil = snoc(q_nil,X0) ),
inference(forward_demodulation,[status(thm)],[f128,f14640]) ).
fof(f14642,plain,
! [X0] :
( ~ sQ756_spl
| q_nil = cons(X0,q_nil) ),
inference(forward_demodulation,[status(thm)],[f135,f14641]) ).
fof(f14643,plain,
( ~ sQ756_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14642,f133]) ).
fof(f14644,plain,
~ sQ756_spl,
inference(contradiction_clause,[status(thm)],[f14643]) ).
fof(f15111,definition,
( sQ770_spl
<=> elem(last(tail(init(q_nil))),q_nil) ),
introduced(definition,[new_symbols(definition,[sQ770_spl])],[split_symbol_definition]) ).
fof(f15112,plain,
( ~ sQ770_spl
| elem(last(tail(init(q_nil))),q_nil) ),
inference(component_clause,[status(thm)],[f15111]) ).
fof(f15128,plain,
( ~ sQ770_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15112,f137]) ).
fof(f15129,plain,
~ sQ770_spl,
inference(contradiction_clause,[status(thm)],[f15128]) ).
fof(f15158,definition,
( sQ778_spl
<=> elem(last(init(q_nil)),q_nil) ),
introduced(definition,[new_symbols(definition,[sQ778_spl])],[split_symbol_definition]) ).
fof(f15159,plain,
( ~ sQ778_spl
| elem(last(init(q_nil)),q_nil) ),
inference(component_clause,[status(thm)],[f15158]) ).
fof(f15169,plain,
( ~ sQ778_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15159,f137]) ).
fof(f15170,plain,
~ sQ778_spl,
inference(contradiction_clause,[status(thm)],[f15169]) ).
fof(f15276,plain,
! [X0,X1] :
( ~ sQ179_spl
| m_Ack(X0,X1) = m_Halt(sK0_skl(m_Ack(X0,X1))) ),
inference(resolution,[status(thm)],[f2652,f84]) ).
fof(f15301,plain,
( ~ sQ179_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15276,f83]) ).
fof(f15302,plain,
~ sQ179_spl,
inference(contradiction_clause,[status(thm)],[f15301]) ).
fof(f16097,definition,
( sQ790_spl
<=> elem(last(init(tail(sK7_skl))),q_nil) ),
introduced(definition,[new_symbols(definition,[sQ790_spl])],[split_symbol_definition]) ).
fof(f16098,plain,
( ~ sQ790_spl
| elem(last(init(tail(sK7_skl))),q_nil) ),
inference(component_clause,[status(thm)],[f16097]) ).
fof(f16114,plain,
( ~ sQ790_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16098,f137]) ).
fof(f16115,plain,
~ sQ790_spl,
inference(contradiction_clause,[status(thm)],[f16114]) ).
fof(f16146,definition,
( sQ798_spl
<=> s(zero) = s(host(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ798_spl])],[split_symbol_definition]) ).
fof(f16147,plain,
( ~ sQ798_spl
| s(zero) = s(host(sK10_skl)) ),
inference(component_clause,[status(thm)],[f16146]) ).
fof(f16165,plain,
( ~ sQ798_spl
| s(zero) = s(host(sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f242,f16147]) ).
fof(f16289,definition,
( sQ802_spl
<=> elem(head(tail(sK7_skl)),q_nil) ),
introduced(definition,[new_symbols(definition,[sQ802_spl])],[split_symbol_definition]) ).
fof(f16290,plain,
( ~ sQ802_spl
| elem(head(tail(sK7_skl)),q_nil) ),
inference(component_clause,[status(thm)],[f16289]) ).
fof(f16299,plain,
( ~ sQ802_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16290,f137]) ).
fof(f16300,plain,
~ sQ802_spl,
inference(contradiction_clause,[status(thm)],[f16299]) ).
fof(f17330,plain,
( ~ sQ671_spl
| ~ leq(s(zero),s(nbr_proc)) ),
inference(paramodulation,[status(thm)],[f13315,f191]) ).
fof(f17341,plain,
( ~ sQ671_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17330,f509]) ).
fof(f17342,plain,
~ sQ671_spl,
inference(contradiction_clause,[status(thm)],[f17341]) ).
fof(f18188,plain,
( ~ sQ798_spl
| ~ leq(s(zero),host(sK8_skl)) ),
inference(paramodulation,[status(thm)],[f16165,f191]) ).
fof(f18192,plain,
( ~ sQ798_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18188,f74]) ).
fof(f18193,plain,
~ sQ798_spl,
inference(contradiction_clause,[status(thm)],[f18192]) ).
fof(f18862,definition,
( sQ821_spl
<=> elem(last(tail(init(sK7_skl))),q_nil) ),
introduced(definition,[new_symbols(definition,[sQ821_spl])],[split_symbol_definition]) ).
fof(f18863,plain,
( ~ sQ821_spl
| elem(last(tail(init(sK7_skl))),q_nil) ),
inference(component_clause,[status(thm)],[f18862]) ).
fof(f18875,plain,
( ~ sQ821_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18863,f137]) ).
fof(f18876,plain,
~ sQ821_spl,
inference(contradiction_clause,[status(thm)],[f18875]) ).
fof(f18926,plain,
! [X0,X1] :
( leq(zero,host(X1))
| leq(zero,host(X0)) ),
inference(resolution,[status(thm)],[f2422,f2384]) ).
fof(f18951,plain,
sQ330_spl,
inference(split_clause,[status(thm)],[f18926,f4502]) ).
fof(f19105,plain,
( ~ sQ732_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14227,f134]) ).
fof(f19106,plain,
~ sQ732_spl,
inference(contradiction_clause,[status(thm)],[f19105]) ).
fof(f19439,plain,
! [X0] :
( ~ sQ203_spl
| ~ sQ279_spl
| ~ elem(m_Ack(sK10_skl,X0),queue(host(sK8_skl)))
| host(sK12_skl) != host(X0) ),
inference(forward_demodulation,[status(thm)],[f4010,f2911]) ).
fof(f19440,plain,
( ~ sQ67_spl
| ~ sQ203_spl
| ~ sQ279_spl
| host(sK12_skl) != host(sK12_skl) ),
inference(resolution,[status(thm)],[f19439,f976]) ).
fof(f19441,plain,
( ~ sQ67_spl
| ~ sQ203_spl
| ~ sQ279_spl
| ~ sQ282_spl ),
inference(split_clause,[status(thm)],[f19440,f4076,f4009,f2910,f975]) ).
fof(f21531,plain,
( ~ sQ174_spl
| ~ sQ91_spl
| leq(nbr_proc,host(sK9_skl))
| nbr_proc = s(host(sK9_skl)) ),
inference(resolution,[status(thm)],[f4005,f208]) ).
fof(f21537,definition,
( sQ848_spl
<=> nbr_proc = s(host(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ848_spl])],[split_symbol_definition]) ).
fof(f21538,plain,
( ~ sQ848_spl
| nbr_proc = s(host(sK9_skl)) ),
inference(component_clause,[status(thm)],[f21537]) ).
fof(f21540,definition,
( sQ849_spl
<=> leq(nbr_proc,host(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ849_spl])],[split_symbol_definition]) ).
fof(f21541,plain,
( ~ sQ849_spl
| leq(nbr_proc,host(sK9_skl)) ),
inference(component_clause,[status(thm)],[f21540]) ).
fof(f21543,plain,
( ~ sQ174_spl
| ~ sQ91_spl
| sQ849_spl
| sQ848_spl ),
inference(split_clause,[status(thm)],[f21531,f21537,f21540,f1151,f2352]) ).
fof(f21548,plain,
( ~ sQ849_spl
| sQ18_spl
| ~ sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21541,f1048]) ).
fof(f21549,plain,
( ~ sQ849_spl
| sQ18_spl
| ~ sQ76_spl ),
inference(contradiction_clause,[status(thm)],[f21548]) ).
fof(f21563,plain,
( ~ sQ848_spl
| ~ sQ91_spl
| ~ leq(nbr_proc,nbr_proc)
| leq(host(sK9_skl),host(sK12_skl)) ),
inference(paramodulation,[status(thm)],[f21538,f3784]) ).
fof(f21582,plain,
( ~ sQ848_spl
| ~ sQ91_spl
| ~ sQ159_spl
| sQ278_spl ),
inference(split_clause,[status(thm)],[f21563,f4006,f1837,f1151,f21537]) ).
fof(f21606,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ76_spl
| sQ456_spl ),
inference(split_clause,[status(thm)],[f3254,f7514,f1038,f468,f412,f420]) ).
fof(f21611,plain,
$false,
inference(sat_refutation,[status(thm)],[f340,f471,f494,f502,f628,f632,f636,f639,f685,f719,f873,f978,f980,f1041,f1043,f1154,f1156,f1310,f1370,f2355,f2913,f3138,f3180,f3476,f3997,f4012,f4150,f4305,f4496,f7346,f8949,f10467,f10469,f11147,f12567,f13046,f13232,f13825,f13851,f13906,f14235,f14353,f14644,f15129,f15170,f15302,f16115,f16300,f17342,f18193,f18876,f18951,f19106,f19441,f21543,f21549,f21582,f21606]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV466+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:52:34 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 66.47/8.98 % Refutation found
% 66.47/8.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 66.47/8.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 66.47/9.06 % Elapsed time: 8.679028 seconds
% 66.47/9.06 % CPU time: 68.160860 seconds
% 66.47/9.06 % Total memory used: 328.227 MB
% 66.47/9.06 % Net memory used: 288.798 MB
%------------------------------------------------------------------------------