%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV473+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:15:54 PM UTC 2026
% Result : Theorem 1.78s 1.14s
% Output : Refutation 4.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 29
% Syntax : Number of formulae : 190 ( 44 unt; 27 def)
% Number of atoms : 1032 ( 346 equ)
% Maximal formula atoms : 67 ( 5 avg)
% Number of connectives : 1415 ( 573 ~; 533 |; 236 &)
% ( 19 <=>; 54 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 32 ( 30 usr; 11 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 20 con; 0-2 aty)
% Number of variables : 403 ( 0 sgn 376 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f47,axiom,
! [X0,X1,X2] :
( elem(X0,cons(X1,X2))
<=> ( X0 = X1
| elem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_46) ).
fof(f67,conjecture,
! [X0,X1,X2,X3] :
( ( ! [X4,X5] :
( elem(m_Ldr(X5),queue(host(X4)))
=> ~ leq(host(X4),host(X5)) )
& ! [X4,X5] :
( elem(m_Down(X5),queue(host(X4)))
=> host(X5) != host(X4) )
& ! [X4,X5] :
( host(X5) = nbr_proc
=> ~ elem(m_NotNorm(X4),queue(host(X5))) )
& ! [X4,X5] :
( ( X5 != X4
& host(X5) = host(X4) )
=> ( ~ setIn(X4,alive)
| ~ setIn(X5,alive) ) )
& ! [X4] :
( ( ( index(status,host(X4)) = elec_1
| index(status,host(X4)) = elec_2 )
& setIn(X4,alive) )
=> index(elid,host(X4)) = X4 )
& ! [X4,X6,X5] :
( ( host(X5) != host(X6)
& setIn(X5,alive)
& host(X5) = host(X4)
& index(status,host(X5)) = norm
& index(ldr,host(X5)) = host(X6) )
=> ~ elem(m_Down(X4),queue(host(X6))) )
& ! [X4,X6,X5] :
( ( host(X5) != host(X6)
& setIn(X5,alive)
& host(X5) = host(X4)
& index(status,host(X5)) = wait
& host(index(elid,host(X5))) = host(X6) )
=> ~ elem(m_Down(X4),queue(host(X6))) )
& ! [X4,X7,X6,X5] :
( ( host(X6) != host(X4)
& setIn(X4,alive)
& setIn(X6,alive)
& host(X7) = host(X4)
& host(X5) = host(X6) )
=> ~ ( elem(m_Down(X5),queue(host(X4)))
& elem(m_Down(X7),queue(host(X6))) ) )
& ! [X4,X7,X6,X5] :
( ( host(X6) != host(X4)
& setIn(X4,alive)
& setIn(X6,alive)
& host(X7) = host(X4)
& host(X5) = host(X6) )
=> ~ ( elem(m_Down(X5),queue(host(X4)))
& setIn(host(X7),index(down,host(X6))) ) )
& ! [X4,X7,X6,X5] :
( ( ! [X8] :
( ( ~ leq(host(X5),X8)
& leq(s(zero),X8) )
=> ( setIn(X8,index(down,host(X5)))
| X8 = host(X6) ) )
& elem(m_Down(X6),queue(host(X5)))
& host(X5) = nbr_proc
& host(X5) = host(X7)
& index(status,host(X5)) = elec_1 )
=> ~ ( setIn(X4,alive)
& elem(m_Down(X7),queue(host(X4))) ) )
& queue(host(X2)) = cons(m_Ack(X1,X3),X0) )
=> ( setIn(X2,alive)
=> ( ~ ( index(elid,host(X2)) = X1
& index(status,host(X2)) = elec_2
& host(X3) = index(pendack,host(X2)) )
=> ! [X4] :
( host(X2) != host(X4)
=> ! [X9,X10,X11] :
( host(X2) = host(X11)
=> ( ( ! [X8] :
( ( ~ leq(host(X11),X8)
& leq(s(zero),X8) )
=> ( setIn(X8,index(down,host(X11)))
| X8 = host(X10) ) )
& elem(m_Down(X10),X0)
& host(X11) = host(X9)
& host(X11) = nbr_proc
& index(status,host(X11)) = elec_1 )
=> ~ ( setIn(X4,alive)
& elem(m_Down(X9),queue(host(X4))) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj) ).
fof(f68,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( ! [X4,X5] :
( elem(m_Ldr(X5),queue(host(X4)))
=> ~ leq(host(X4),host(X5)) )
& ! [X4,X5] :
( elem(m_Down(X5),queue(host(X4)))
=> host(X5) != host(X4) )
& ! [X4,X5] :
( host(X5) = nbr_proc
=> ~ elem(m_NotNorm(X4),queue(host(X5))) )
& ! [X4,X5] :
( ( X5 != X4
& host(X5) = host(X4) )
=> ( ~ setIn(X4,alive)
| ~ setIn(X5,alive) ) )
& ! [X4] :
( ( ( index(status,host(X4)) = elec_1
| index(status,host(X4)) = elec_2 )
& setIn(X4,alive) )
=> index(elid,host(X4)) = X4 )
& ! [X4,X6,X5] :
( ( host(X5) != host(X6)
& setIn(X5,alive)
& host(X5) = host(X4)
& index(status,host(X5)) = norm
& index(ldr,host(X5)) = host(X6) )
=> ~ elem(m_Down(X4),queue(host(X6))) )
& ! [X4,X6,X5] :
( ( host(X5) != host(X6)
& setIn(X5,alive)
& host(X5) = host(X4)
& index(status,host(X5)) = wait
& host(index(elid,host(X5))) = host(X6) )
=> ~ elem(m_Down(X4),queue(host(X6))) )
& ! [X4,X7,X6,X5] :
( ( host(X6) != host(X4)
& setIn(X4,alive)
& setIn(X6,alive)
& host(X7) = host(X4)
& host(X5) = host(X6) )
=> ~ ( elem(m_Down(X5),queue(host(X4)))
& elem(m_Down(X7),queue(host(X6))) ) )
& ! [X4,X7,X6,X5] :
( ( host(X6) != host(X4)
& setIn(X4,alive)
& setIn(X6,alive)
& host(X7) = host(X4)
& host(X5) = host(X6) )
=> ~ ( elem(m_Down(X5),queue(host(X4)))
& setIn(host(X7),index(down,host(X6))) ) )
& ! [X4,X7,X6,X5] :
( ( ! [X8] :
( ( ~ leq(host(X5),X8)
& leq(s(zero),X8) )
=> ( setIn(X8,index(down,host(X5)))
| X8 = host(X6) ) )
& elem(m_Down(X6),queue(host(X5)))
& host(X5) = nbr_proc
& host(X5) = host(X7)
& index(status,host(X5)) = elec_1 )
=> ~ ( setIn(X4,alive)
& elem(m_Down(X7),queue(host(X4))) ) )
& queue(host(X2)) = cons(m_Ack(X1,X3),X0) )
=> ( setIn(X2,alive)
=> ( ~ ( index(elid,host(X2)) = X1
& index(status,host(X2)) = elec_2
& host(X3) = index(pendack,host(X2)) )
=> ! [X4] :
( host(X2) != host(X4)
=> ! [X9,X10,X11] :
( host(X2) = host(X11)
=> ( ( ! [X8] :
( ( ~ leq(host(X11),X8)
& leq(s(zero),X8) )
=> ( setIn(X8,index(down,host(X11)))
| X8 = host(X10) ) )
& elem(m_Down(X10),X0)
& host(X11) = host(X9)
& host(X11) = nbr_proc
& index(status,host(X11)) = elec_1 )
=> ~ ( setIn(X4,alive)
& elem(m_Down(X9),queue(host(X4))) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f67]) ).
fof(f69,plain,
~ ! [X0,X1,X2,X3] :
( ( ! [X4,X5] :
( elem(m_Ldr(X5),queue(host(X4)))
=> ~ leq(host(X4),host(X5)) )
& ! [X6,X7] :
( elem(m_Down(X7),queue(host(X6)))
=> host(X6) != host(X7) )
& ! [X8,X9] :
( nbr_proc = host(X9)
=> ~ elem(m_NotNorm(X8),queue(host(X9))) )
& ! [X10,X11] :
( ( X10 != X11
& host(X11) = host(X10) )
=> ( ~ setIn(X10,alive)
| ~ setIn(X11,alive) ) )
& ! [X12] :
( ( ( elec_1 = index(status,host(X12))
| elec_2 = index(status,host(X12)) )
& setIn(X12,alive) )
=> index(elid,host(X12)) = X12 )
& ! [X13,X14,X15] :
( ( host(X15) != host(X14)
& setIn(X15,alive)
& host(X15) = host(X13)
& norm = index(status,host(X15))
& host(X14) = index(ldr,host(X15)) )
=> ~ elem(m_Down(X13),queue(host(X14))) )
& ! [X16,X17,X18] :
( ( host(X18) != host(X17)
& setIn(X18,alive)
& host(X18) = host(X16)
& wait = index(status,host(X18))
& host(X17) = host(index(elid,host(X18))) )
=> ~ elem(m_Down(X16),queue(host(X17))) )
& ! [X19,X20,X21,X22] :
( ( host(X19) != host(X21)
& setIn(X19,alive)
& setIn(X21,alive)
& host(X19) = host(X20)
& host(X21) = host(X22) )
=> ~ ( elem(m_Down(X22),queue(host(X19)))
& elem(m_Down(X20),queue(host(X21))) ) )
& ! [X23,X24,X25,X26] :
( ( host(X23) != host(X25)
& setIn(X23,alive)
& setIn(X25,alive)
& host(X23) = host(X24)
& host(X25) = host(X26) )
=> ~ ( elem(m_Down(X26),queue(host(X23)))
& setIn(host(X24),index(down,host(X25))) ) )
& ! [X27,X28,X29,X30] :
( ( ! [X31] :
( ( ~ leq(host(X30),X31)
& leq(s(zero),X31) )
=> ( setIn(X31,index(down,host(X30)))
| host(X29) = X31 ) )
& elem(m_Down(X29),queue(host(X30)))
& nbr_proc = host(X30)
& host(X30) = host(X28)
& elec_1 = index(status,host(X30)) )
=> ~ ( setIn(X27,alive)
& elem(m_Down(X28),queue(host(X27))) ) )
& queue(host(X2)) = cons(m_Ack(X1,X3),X0) )
=> ( setIn(X2,alive)
=> ( ~ ( index(elid,host(X2)) = X1
& index(status,host(X2)) = elec_2
& host(X3) = index(pendack,host(X2)) )
=> ! [X32] :
( host(X2) != host(X32)
=> ! [X33,X34,X35] :
( host(X2) = host(X35)
=> ( ( ! [X36] :
( ( ~ leq(host(X35),X36)
& leq(s(zero),X36) )
=> ( setIn(X36,index(down,host(X35)))
| host(X34) = X36 ) )
& elem(m_Down(X34),X0)
& host(X35) = host(X33)
& nbr_proc = host(X35)
& elec_1 = index(status,host(X35)) )
=> ~ ( setIn(X32,alive)
& elem(m_Down(X33),queue(host(X32))) ) ) ) ) ) ) ),
inference(rectify,[],[f68]) ).
fof(f70,plain,
? [X0,X1,X2,X3] :
( ? [X32] :
( ? [X33,X34,X35] :
( setIn(X32,alive)
& elem(m_Down(X33),queue(host(X32)))
& ! [X36] :
( setIn(X36,index(down,host(X35)))
| host(X34) = X36
| leq(host(X35),X36)
| ~ leq(s(zero),X36) )
& elem(m_Down(X34),X0)
& host(X35) = host(X33)
& nbr_proc = host(X35)
& elec_1 = index(status,host(X35))
& host(X2) = host(X35) )
& host(X2) != host(X32) )
& ( index(elid,host(X2)) != X1
| elec_2 != index(status,host(X2))
| host(X3) != index(pendack,host(X2)) )
& setIn(X2,alive)
& ! [X4,X5] :
( ~ leq(host(X4),host(X5))
| ~ elem(m_Ldr(X5),queue(host(X4))) )
& ! [X6,X7] :
( host(X6) != host(X7)
| ~ elem(m_Down(X7),queue(host(X6))) )
& ! [X8,X9] :
( ~ elem(m_NotNorm(X8),queue(host(X9)))
| nbr_proc != host(X9) )
& ! [X10,X11] :
( ~ setIn(X10,alive)
| ~ setIn(X11,alive)
| X10 = X11
| host(X11) != host(X10) )
& ! [X12] :
( index(elid,host(X12)) = X12
| ( elec_1 != index(status,host(X12))
& elec_2 != index(status,host(X12)) )
| ~ setIn(X12,alive) )
& ! [X13,X14,X15] :
( ~ elem(m_Down(X13),queue(host(X14)))
| host(X15) = host(X14)
| ~ setIn(X15,alive)
| host(X15) != host(X13)
| norm != index(status,host(X15))
| host(X14) != index(ldr,host(X15)) )
& ! [X16,X17,X18] :
( ~ elem(m_Down(X16),queue(host(X17)))
| host(X18) = host(X17)
| ~ setIn(X18,alive)
| host(X18) != host(X16)
| wait != index(status,host(X18))
| host(X17) != host(index(elid,host(X18))) )
& ! [X19,X20,X21,X22] :
( ~ elem(m_Down(X22),queue(host(X19)))
| ~ elem(m_Down(X20),queue(host(X21)))
| host(X19) = host(X21)
| ~ setIn(X19,alive)
| ~ setIn(X21,alive)
| host(X19) != host(X20)
| host(X21) != host(X22) )
& ! [X23,X24,X25,X26] :
( ~ elem(m_Down(X26),queue(host(X23)))
| ~ setIn(host(X24),index(down,host(X25)))
| host(X23) = host(X25)
| ~ setIn(X23,alive)
| ~ setIn(X25,alive)
| host(X23) != host(X24)
| host(X25) != host(X26) )
& ! [X27,X28,X29,X30] :
( ~ setIn(X27,alive)
| ~ elem(m_Down(X28),queue(host(X27)))
| ? [X31] :
( ~ setIn(X31,index(down,host(X30)))
& host(X29) != X31
& ~ leq(host(X30),X31)
& leq(s(zero),X31) )
| ~ elem(m_Down(X29),queue(host(X30)))
| nbr_proc != host(X30)
| host(X30) != host(X28)
| elec_1 != index(status,host(X30)) )
& queue(host(X2)) = cons(m_Ack(X1,X3),X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f71,plain,
? [X0,X1,X2,X3] :
( ? [X32] :
( ? [X33,X34,X35] :
( setIn(X32,alive)
& elem(m_Down(X33),queue(host(X32)))
& ! [X36] :
( setIn(X36,index(down,host(X35)))
| host(X34) = X36
| leq(host(X35),X36)
| ~ leq(s(zero),X36) )
& elem(m_Down(X34),X0)
& host(X35) = host(X33)
& nbr_proc = host(X35)
& elec_1 = index(status,host(X35))
& host(X2) = host(X35) )
& host(X2) != host(X32) )
& ( index(elid,host(X2)) != X1
| elec_2 != index(status,host(X2))
| host(X3) != index(pendack,host(X2)) )
& setIn(X2,alive)
& ! [X4,X5] :
( ~ leq(host(X4),host(X5))
| ~ elem(m_Ldr(X5),queue(host(X4))) )
& ! [X6,X7] :
( host(X6) != host(X7)
| ~ elem(m_Down(X7),queue(host(X6))) )
& ! [X8,X9] :
( ~ elem(m_NotNorm(X8),queue(host(X9)))
| nbr_proc != host(X9) )
& ! [X10,X11] :
( ~ setIn(X10,alive)
| ~ setIn(X11,alive)
| X10 = X11
| host(X11) != host(X10) )
& ! [X12] :
( index(elid,host(X12)) = X12
| ( elec_1 != index(status,host(X12))
& elec_2 != index(status,host(X12)) )
| ~ setIn(X12,alive) )
& ! [X13,X14,X15] :
( ~ elem(m_Down(X13),queue(host(X14)))
| host(X15) = host(X14)
| ~ setIn(X15,alive)
| host(X15) != host(X13)
| norm != index(status,host(X15))
| host(X14) != index(ldr,host(X15)) )
& ! [X16,X17,X18] :
( ~ elem(m_Down(X16),queue(host(X17)))
| host(X18) = host(X17)
| ~ setIn(X18,alive)
| host(X18) != host(X16)
| wait != index(status,host(X18))
| host(X17) != host(index(elid,host(X18))) )
& ! [X19,X20,X21,X22] :
( ~ elem(m_Down(X22),queue(host(X19)))
| ~ elem(m_Down(X20),queue(host(X21)))
| host(X19) = host(X21)
| ~ setIn(X19,alive)
| ~ setIn(X21,alive)
| host(X19) != host(X20)
| host(X21) != host(X22) )
& ! [X23,X24,X25,X26] :
( ~ elem(m_Down(X26),queue(host(X23)))
| ~ setIn(host(X24),index(down,host(X25)))
| host(X23) = host(X25)
| ~ setIn(X23,alive)
| ~ setIn(X25,alive)
| host(X23) != host(X24)
| host(X25) != host(X26) )
& ! [X27,X28,X29,X30] :
( ~ setIn(X27,alive)
| ~ elem(m_Down(X28),queue(host(X27)))
| ? [X31] :
( ~ setIn(X31,index(down,host(X30)))
& host(X29) != X31
& ~ leq(host(X30),X31)
& leq(s(zero),X31) )
| ~ elem(m_Down(X29),queue(host(X30)))
| nbr_proc != host(X30)
| host(X30) != host(X28)
| elec_1 != index(status,host(X30)) )
& queue(host(X2)) = cons(m_Ack(X1,X3),X0) ),
inference(flattening,[],[f70]) ).
fof(f78,plain,
? [X0,X1,X2,X3] :
( ? [X4] :
( ? [X5,X6,X7] :
( setIn(X4,alive)
& elem(m_Down(X5),queue(host(X4)))
& ! [X8] :
( setIn(X8,index(down,host(X7)))
| host(X6) = X8
| leq(host(X7),X8)
| ~ leq(s(zero),X8) )
& elem(m_Down(X6),X0)
& host(X5) = host(X7)
& nbr_proc = host(X7)
& elec_1 = index(status,host(X7))
& host(X2) = host(X7) )
& host(X2) != host(X4) )
& ( index(elid,host(X2)) != X1
| elec_2 != index(status,host(X2))
| host(X3) != index(pendack,host(X2)) )
& setIn(X2,alive)
& ! [X9,X10] :
( ~ leq(host(X9),host(X10))
| ~ elem(m_Ldr(X10),queue(host(X9))) )
& ! [X11,X12] :
( host(X11) != host(X12)
| ~ elem(m_Down(X12),queue(host(X11))) )
& ! [X13,X14] :
( ~ elem(m_NotNorm(X13),queue(host(X14)))
| nbr_proc != host(X14) )
& ! [X15,X16] :
( ~ setIn(X15,alive)
| ~ setIn(X16,alive)
| X15 = X16
| host(X15) != host(X16) )
& ! [X17] :
( index(elid,host(X17)) = X17
| ( elec_1 != index(status,host(X17))
& elec_2 != index(status,host(X17)) )
| ~ setIn(X17,alive) )
& ! [X18,X19,X20] :
( ~ elem(m_Down(X18),queue(host(X19)))
| host(X19) = host(X20)
| ~ setIn(X20,alive)
| host(X18) != host(X20)
| norm != index(status,host(X20))
| host(X19) != index(ldr,host(X20)) )
& ! [X21,X22,X23] :
( ~ elem(m_Down(X21),queue(host(X22)))
| host(X22) = host(X23)
| ~ setIn(X23,alive)
| host(X21) != host(X23)
| wait != index(status,host(X23))
| host(X22) != host(index(elid,host(X23))) )
& ! [X24,X25,X26,X27] :
( ~ elem(m_Down(X27),queue(host(X24)))
| ~ elem(m_Down(X25),queue(host(X26)))
| host(X24) = host(X26)
| ~ setIn(X24,alive)
| ~ setIn(X26,alive)
| host(X25) != host(X24)
| host(X26) != host(X27) )
& ! [X28,X29,X30,X31] :
( ~ elem(m_Down(X31),queue(host(X28)))
| ~ setIn(host(X29),index(down,host(X30)))
| host(X30) = host(X28)
| ~ setIn(X28,alive)
| ~ setIn(X30,alive)
| host(X29) != host(X28)
| host(X30) != host(X31) )
& ! [X32,X33,X34,X35] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| ? [X36] :
( ~ setIn(X36,index(down,host(X35)))
& host(X34) != X36
& ~ leq(host(X35),X36)
& leq(s(zero),X36) )
| ~ elem(m_Down(X34),queue(host(X35)))
| nbr_proc != host(X35)
| host(X35) != host(X33)
| elec_1 != index(status,host(X35)) )
& queue(host(X2)) = cons(m_Ack(X1,X3),X0) ),
inference(rectify,[],[f71]) ).
fof(f79,plain,
( setIn(sK4,alive)
& elem(m_Down(sK5),queue(host(sK4)))
& ! [X8] :
( setIn(X8,index(down,host(sK7)))
| host(sK6) = X8
| leq(host(sK7),X8)
| ~ leq(s(zero),X8) )
& elem(m_Down(sK6),sK0)
& host(sK7) = host(sK5)
& nbr_proc = host(sK7)
& elec_1 = index(status,host(sK7))
& host(sK7) = host(sK2)
& host(sK4) != host(sK2)
& ( sK1 != index(elid,host(sK2))
| elec_2 != index(status,host(sK2))
| host(sK3) != index(pendack,host(sK2)) )
& setIn(sK2,alive)
& ! [X9,X10] :
( ~ leq(host(X9),host(X10))
| ~ elem(m_Ldr(X10),queue(host(X9))) )
& ! [X11,X12] :
( host(X11) != host(X12)
| ~ elem(m_Down(X12),queue(host(X11))) )
& ! [X13,X14] :
( ~ elem(m_NotNorm(X13),queue(host(X14)))
| nbr_proc != host(X14) )
& ! [X15,X16] :
( ~ setIn(X15,alive)
| ~ setIn(X16,alive)
| X15 = X16
| host(X15) != host(X16) )
& ! [X17] :
( index(elid,host(X17)) = X17
| ( elec_1 != index(status,host(X17))
& elec_2 != index(status,host(X17)) )
| ~ setIn(X17,alive) )
& ! [X18,X19,X20] :
( ~ elem(m_Down(X18),queue(host(X19)))
| host(X19) = host(X20)
| ~ setIn(X20,alive)
| host(X18) != host(X20)
| norm != index(status,host(X20))
| host(X19) != index(ldr,host(X20)) )
& ! [X21,X22,X23] :
( ~ elem(m_Down(X21),queue(host(X22)))
| host(X22) = host(X23)
| ~ setIn(X23,alive)
| host(X21) != host(X23)
| wait != index(status,host(X23))
| host(X22) != host(index(elid,host(X23))) )
& ! [X24,X25,X26,X27] :
( ~ elem(m_Down(X27),queue(host(X24)))
| ~ elem(m_Down(X25),queue(host(X26)))
| host(X24) = host(X26)
| ~ setIn(X24,alive)
| ~ setIn(X26,alive)
| host(X25) != host(X24)
| host(X26) != host(X27) )
& ! [X28,X29,X30,X31] :
( ~ elem(m_Down(X31),queue(host(X28)))
| ~ setIn(host(X29),index(down,host(X30)))
| host(X30) = host(X28)
| ~ setIn(X28,alive)
| ~ setIn(X30,alive)
| host(X29) != host(X28)
| host(X30) != host(X31) )
& ! [X32,X33,X34,X35] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| ( ~ setIn(sK8(X34,X35),index(down,host(X35)))
& host(X34) != sK8(X34,X35)
& ~ leq(host(X35),sK8(X34,X35))
& leq(s(zero),sK8(X34,X35)) )
| ~ elem(m_Down(X34),queue(host(X35)))
| nbr_proc != host(X35)
| host(X35) != host(X33)
| elec_1 != index(status,host(X35)) )
& queue(host(sK2)) = cons(m_Ack(sK1,sK3),sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7),skolemize(X36,sK8(X34,X35))],[f78]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ( elem(X0,cons(X1,X2))
| ( X0 != X1
& ~ elem(X0,X2) ) )
& ( X0 = X1
| elem(X0,X2)
| ~ elem(X0,cons(X1,X2)) ) ),
inference(nnf_transformation,[],[f47]) ).
fof(f83,plain,
! [X0,X1,X2] :
( ( elem(X0,cons(X1,X2))
| ( X0 != X1
& ~ elem(X0,X2) ) )
& ( X0 = X1
| elem(X0,X2)
| ~ elem(X0,cons(X1,X2)) ) ),
inference(flattening,[],[f82]) ).
fof(f92,plain,
queue(host(sK2)) = cons(m_Ack(sK1,sK3),sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f93,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| leq(s(zero),sK8(X34,X35))
| ~ elem(m_Down(X34),queue(host(X35)))
| nbr_proc != host(X35)
| host(X35) != host(X33)
| elec_1 != index(status,host(X35)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f94,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| ~ leq(host(X35),sK8(X34,X35))
| ~ elem(m_Down(X34),queue(host(X35)))
| nbr_proc != host(X35)
| host(X35) != host(X33)
| elec_1 != index(status,host(X35)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f95,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| host(X34) != sK8(X34,X35)
| ~ elem(m_Down(X34),queue(host(X35)))
| nbr_proc != host(X35)
| host(X35) != host(X33)
| elec_1 != index(status,host(X35)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f96,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| ~ setIn(sK8(X34,X35),index(down,host(X35)))
| ~ elem(m_Down(X34),queue(host(X35)))
| nbr_proc != host(X35)
| host(X35) != host(X33)
| elec_1 != index(status,host(X35)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f102,plain,
! [X17] :
( index(elid,host(X17)) = X17
| elec_1 != index(status,host(X17))
| ~ setIn(X17,alive) ),
inference(cnf_transformation,[],[f79]) ).
fof(f107,plain,
setIn(sK2,alive),
inference(cnf_transformation,[],[f79]) ).
fof(f110,plain,
host(sK7) = host(sK2),
inference(cnf_transformation,[],[f79]) ).
fof(f111,plain,
elec_1 = index(status,host(sK7)),
inference(cnf_transformation,[],[f79]) ).
fof(f112,plain,
nbr_proc = host(sK7),
inference(cnf_transformation,[],[f79]) ).
fof(f113,plain,
host(sK7) = host(sK5),
inference(cnf_transformation,[],[f79]) ).
fof(f114,plain,
elem(m_Down(sK6),sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f115,plain,
! [X8] :
( setIn(X8,index(down,host(sK7)))
| host(sK6) = X8
| leq(host(sK7),X8)
| ~ leq(s(zero),X8) ),
inference(cnf_transformation,[],[f79]) ).
fof(f116,plain,
elem(m_Down(sK5),queue(host(sK4))),
inference(cnf_transformation,[],[f79]) ).
fof(f117,plain,
setIn(sK4,alive),
inference(cnf_transformation,[],[f79]) ).
fof(f125,plain,
! [X2,X0,X1] :
( elem(X0,cons(X1,X2))
| ~ elem(X0,X2) ),
inference(cnf_transformation,[],[f83]) ).
fof(f173,definition,
~ sP14(elec_1),
introduced(definition,[new_symbols(definition,[sP14])],[inequality_splitting_name_introduction]) ).
fof(f174,plain,
! [X17] :
( index(elid,host(X17)) = X17
| sP14(index(status,host(X17)))
| ~ setIn(X17,alive) ),
inference(inequality_splitting,[],[f102,f173]) ).
fof(f181,definition,
~ sP18(nbr_proc),
introduced(definition,[new_symbols(definition,[sP18])],[inequality_splitting_name_introduction]) ).
fof(f182,definition,
~ sP19(elec_1),
introduced(definition,[new_symbols(definition,[sP19])],[inequality_splitting_name_introduction]) ).
fof(f183,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| ~ setIn(sK8(X34,X35),index(down,host(X35)))
| ~ elem(m_Down(X34),queue(host(X35)))
| sP18(host(X35))
| host(X35) != host(X33)
| sP19(index(status,host(X35))) ),
inference(inequality_splitting,[],[f96,f182,f181]) ).
fof(f184,definition,
~ sP20(nbr_proc),
introduced(definition,[new_symbols(definition,[sP20])],[inequality_splitting_name_introduction]) ).
fof(f185,definition,
~ sP21(elec_1),
introduced(definition,[new_symbols(definition,[sP21])],[inequality_splitting_name_introduction]) ).
fof(f186,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| host(X34) != sK8(X34,X35)
| ~ elem(m_Down(X34),queue(host(X35)))
| sP20(host(X35))
| host(X35) != host(X33)
| sP21(index(status,host(X35))) ),
inference(inequality_splitting,[],[f95,f185,f184]) ).
fof(f187,definition,
~ sP22(nbr_proc),
introduced(definition,[new_symbols(definition,[sP22])],[inequality_splitting_name_introduction]) ).
fof(f188,definition,
~ sP23(elec_1),
introduced(definition,[new_symbols(definition,[sP23])],[inequality_splitting_name_introduction]) ).
fof(f189,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| ~ leq(host(X35),sK8(X34,X35))
| ~ elem(m_Down(X34),queue(host(X35)))
| sP22(host(X35))
| host(X35) != host(X33)
| sP23(index(status,host(X35))) ),
inference(inequality_splitting,[],[f94,f188,f187]) ).
fof(f190,definition,
~ sP24(nbr_proc),
introduced(definition,[new_symbols(definition,[sP24])],[inequality_splitting_name_introduction]) ).
fof(f191,definition,
~ sP25(elec_1),
introduced(definition,[new_symbols(definition,[sP25])],[inequality_splitting_name_introduction]) ).
fof(f192,plain,
! [X34,X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| leq(s(zero),sK8(X34,X35))
| ~ elem(m_Down(X34),queue(host(X35)))
| sP24(host(X35))
| host(X35) != host(X33)
| sP25(index(status,host(X35))) ),
inference(inequality_splitting,[],[f93,f191,f190]) ).
fof(f218,plain,
! [X34,X35] :
( ~ setIn(sK8(X34,X35),index(down,host(X35)))
| ~ elem(m_Down(X34),queue(host(X35)))
| sP34(X35) ),
inference(cnf_transformation,[],[f218_D]) ).
fof(f218_D,definition,
! [X35] :
( ! [X34] :
( ~ setIn(sK8(X34,X35),index(down,host(X35)))
| ~ elem(m_Down(X34),queue(host(X35))) )
<=> ~ sP34(X35) ),
introduced(definition,[new_symbols(definition,[sP34])],[general_splitting_component_introduction]) ).
fof(f219,plain,
! [X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| sP18(host(X35))
| host(X35) != host(X33)
| sP19(index(status,host(X35)))
| ~ sP34(X35) ),
inference(general_splitting,[],[f183,f218_D]) ).
fof(f220,plain,
! [X35,X33] :
( host(X35) != host(X33)
| sP18(host(X35))
| sP19(index(status,host(X35)))
| ~ sP34(X35)
| sP35(X33) ),
inference(cnf_transformation,[],[f220_D]) ).
fof(f220_D,definition,
! [X33] :
( ! [X35] :
( host(X35) != host(X33)
| sP18(host(X35))
| sP19(index(status,host(X35)))
| ~ sP34(X35) )
<=> ~ sP35(X33) ),
introduced(definition,[new_symbols(definition,[sP35])],[general_splitting_component_introduction]) ).
fof(f221,plain,
! [X32,X33] :
( ~ elem(m_Down(X33),queue(host(X32)))
| ~ setIn(X32,alive)
| ~ sP35(X33) ),
inference(general_splitting,[],[f219,f220_D]) ).
fof(f222,plain,
! [X34,X35] :
( host(X34) != sK8(X34,X35)
| ~ elem(m_Down(X34),queue(host(X35)))
| sP36(X35) ),
inference(cnf_transformation,[],[f222_D]) ).
fof(f222_D,definition,
! [X35] :
( ! [X34] :
( host(X34) != sK8(X34,X35)
| ~ elem(m_Down(X34),queue(host(X35))) )
<=> ~ sP36(X35) ),
introduced(definition,[new_symbols(definition,[sP36])],[general_splitting_component_introduction]) ).
fof(f223,plain,
! [X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| sP20(host(X35))
| host(X35) != host(X33)
| sP21(index(status,host(X35)))
| ~ sP36(X35) ),
inference(general_splitting,[],[f186,f222_D]) ).
fof(f224,plain,
! [X35,X33] :
( host(X35) != host(X33)
| sP20(host(X35))
| sP21(index(status,host(X35)))
| ~ sP36(X35)
| sP37(X33) ),
inference(cnf_transformation,[],[f224_D]) ).
fof(f224_D,definition,
! [X33] :
( ! [X35] :
( host(X35) != host(X33)
| sP20(host(X35))
| sP21(index(status,host(X35)))
| ~ sP36(X35) )
<=> ~ sP37(X33) ),
introduced(definition,[new_symbols(definition,[sP37])],[general_splitting_component_introduction]) ).
fof(f225,plain,
! [X32,X33] :
( ~ elem(m_Down(X33),queue(host(X32)))
| ~ setIn(X32,alive)
| ~ sP37(X33) ),
inference(general_splitting,[],[f223,f224_D]) ).
fof(f226,plain,
! [X34,X35] :
( ~ leq(host(X35),sK8(X34,X35))
| ~ elem(m_Down(X34),queue(host(X35)))
| sP38(X35) ),
inference(cnf_transformation,[],[f226_D]) ).
fof(f226_D,definition,
! [X35] :
( ! [X34] :
( ~ leq(host(X35),sK8(X34,X35))
| ~ elem(m_Down(X34),queue(host(X35))) )
<=> ~ sP38(X35) ),
introduced(definition,[new_symbols(definition,[sP38])],[general_splitting_component_introduction]) ).
fof(f227,plain,
! [X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| sP22(host(X35))
| host(X35) != host(X33)
| sP23(index(status,host(X35)))
| ~ sP38(X35) ),
inference(general_splitting,[],[f189,f226_D]) ).
fof(f228,plain,
! [X35,X33] :
( host(X35) != host(X33)
| sP22(host(X35))
| sP23(index(status,host(X35)))
| ~ sP38(X35)
| sP39(X33) ),
inference(cnf_transformation,[],[f228_D]) ).
fof(f228_D,definition,
! [X33] :
( ! [X35] :
( host(X35) != host(X33)
| sP22(host(X35))
| sP23(index(status,host(X35)))
| ~ sP38(X35) )
<=> ~ sP39(X33) ),
introduced(definition,[new_symbols(definition,[sP39])],[general_splitting_component_introduction]) ).
fof(f229,plain,
! [X32,X33] :
( ~ elem(m_Down(X33),queue(host(X32)))
| ~ setIn(X32,alive)
| ~ sP39(X33) ),
inference(general_splitting,[],[f227,f228_D]) ).
fof(f230,plain,
! [X34,X35] :
( ~ elem(m_Down(X34),queue(host(X35)))
| leq(s(zero),sK8(X34,X35))
| sP40(X35) ),
inference(cnf_transformation,[],[f230_D]) ).
fof(f230_D,definition,
! [X35] :
( ! [X34] :
( ~ elem(m_Down(X34),queue(host(X35)))
| leq(s(zero),sK8(X34,X35)) )
<=> ~ sP40(X35) ),
introduced(definition,[new_symbols(definition,[sP40])],[general_splitting_component_introduction]) ).
fof(f231,plain,
! [X35,X32,X33] :
( ~ setIn(X32,alive)
| ~ elem(m_Down(X33),queue(host(X32)))
| sP24(host(X35))
| host(X35) != host(X33)
| sP25(index(status,host(X35)))
| ~ sP40(X35) ),
inference(general_splitting,[],[f192,f230_D]) ).
fof(f232,plain,
! [X35,X33] :
( host(X35) != host(X33)
| sP24(host(X35))
| sP25(index(status,host(X35)))
| ~ sP40(X35)
| sP41(X33) ),
inference(cnf_transformation,[],[f232_D]) ).
fof(f232_D,definition,
! [X33] :
( ! [X35] :
( host(X35) != host(X33)
| sP24(host(X35))
| sP25(index(status,host(X35)))
| ~ sP40(X35) )
<=> ~ sP41(X33) ),
introduced(definition,[new_symbols(definition,[sP41])],[general_splitting_component_introduction]) ).
fof(f233,plain,
! [X32,X33] :
( ~ elem(m_Down(X33),queue(host(X32)))
| ~ setIn(X32,alive)
| ~ sP41(X33) ),
inference(general_splitting,[],[f231,f232_D]) ).
fof(f247,plain,
elec_1 = index(status,host(sK2)),
inference(forward_demodulation,[],[f111,f110]) ).
fof(f248,plain,
host(sK5) = host(sK2),
inference(forward_demodulation,[],[f113,f110]) ).
fof(f249,plain,
! [X8] :
( setIn(X8,index(down,host(sK2)))
| host(sK6) = X8
| leq(host(sK7),X8)
| ~ leq(s(zero),X8) ),
inference(forward_demodulation,[],[f115,f110]) ).
fof(f250,plain,
! [X8] :
( setIn(X8,index(down,host(sK2)))
| leq(host(sK2),X8)
| host(sK6) = X8
| ~ leq(s(zero),X8) ),
inference(forward_demodulation,[],[f249,f110]) ).
fof(f257,plain,
nbr_proc = host(sK2),
inference(superposition,[],[f112,f110]) ).
fof(f271,plain,
elec_1 = index(status,nbr_proc),
inference(superposition,[],[f247,f257]) ).
fof(f273,plain,
! [X0] :
( elem(X0,queue(host(sK2)))
| ~ elem(X0,sK0) ),
inference(superposition,[],[f125,f92]) ).
fof(f276,plain,
! [X0] :
( elem(X0,queue(nbr_proc))
| ~ elem(X0,sK0) ),
inference(forward_demodulation,[],[f273,f257]) ).
fof(f305,plain,
( ~ setIn(sK4,alive)
| ~ sP35(sK5) ),
inference(resolution,[],[f221,f116]) ).
fof(f321,plain,
~ sP35(sK5),
inference(forward_subsumption_resolution,[],[f305,f117]) ).
fof(f329,plain,
( ~ setIn(sK4,alive)
| ~ sP37(sK5) ),
inference(resolution,[],[f225,f116]) ).
fof(f341,plain,
~ sP37(sK5),
inference(forward_subsumption_resolution,[],[f329,f117]) ).
fof(f345,plain,
( ~ setIn(sK4,alive)
| ~ sP39(sK5) ),
inference(resolution,[],[f229,f116]) ).
fof(f357,plain,
~ sP39(sK5),
inference(forward_subsumption_resolution,[],[f345,f117]) ).
fof(f361,plain,
( ~ setIn(sK4,alive)
| ~ sP41(sK5) ),
inference(resolution,[],[f233,f116]) ).
fof(f373,plain,
~ sP41(sK5),
inference(forward_subsumption_resolution,[],[f361,f117]) ).
fof(f407,plain,
( sK2 = index(elid,nbr_proc)
| sP14(index(status,nbr_proc))
| ~ setIn(sK2,alive) ),
inference(superposition,[],[f174,f257]) ).
fof(f409,plain,
( sK2 = index(elid,nbr_proc)
| sP14(index(status,nbr_proc)) ),
inference(forward_subsumption_resolution,[],[f407,f107]) ).
fof(f410,plain,
( sP14(elec_1)
| sK2 = index(elid,nbr_proc) ),
inference(forward_demodulation,[],[f409,f271]) ).
fof(f411,plain,
sK2 = index(elid,nbr_proc),
inference(forward_subsumption_resolution,[],[f410,f173]) ).
fof(f456,plain,
nbr_proc = host(index(elid,nbr_proc)),
inference(superposition,[],[f257,f411]) ).
fof(f463,plain,
! [X0] :
( ~ leq(nbr_proc,sK8(X0,sK2))
| ~ elem(m_Down(X0),queue(nbr_proc))
| sP38(sK2) ),
inference(superposition,[],[f226,f257]) ).
fof(f466,plain,
! [X0] :
( ~ leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc))
| sP38(sK2) ),
inference(forward_demodulation,[],[f463,f411]) ).
fof(f477,plain,
! [X0] :
( sP38(index(elid,nbr_proc))
| ~ leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc)) ),
inference(forward_demodulation,[],[f466,f411]) ).
fof(f488,definition,
( spl42_16
<=> ! [X0] :
( ~ leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc)) ) ),
introduced(definition,[new_symbols(definition,[spl42_16])],[avatar_definition]) ).
fof(f489,plain,
( ! [X0] :
( ~ leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc)) )
| ~ spl42_16 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f491,definition,
( spl42_17
<=> sP38(index(elid,nbr_proc)) ),
introduced(definition,[new_symbols(definition,[spl42_17])],[avatar_definition]) ).
fof(f494,plain,
( spl42_16
| spl42_17 ),
inference(avatar_split_clause,[],[f477,f491,f488]) ).
fof(f499,plain,
! [X0] :
( ~ elem(m_Down(X0),queue(nbr_proc))
| leq(s(zero),sK8(X0,sK2))
| sP40(sK2) ),
inference(superposition,[],[f230,f257]) ).
fof(f502,plain,
! [X0] :
( leq(s(zero),sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc))
| sP40(sK2) ),
inference(forward_demodulation,[],[f499,f411]) ).
fof(f529,plain,
! [X0] :
( sP40(index(elid,nbr_proc))
| leq(s(zero),sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc)) ),
inference(forward_demodulation,[],[f502,f411]) ).
fof(f532,definition,
( spl42_24
<=> ! [X0] :
( leq(s(zero),sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc)) ) ),
introduced(definition,[new_symbols(definition,[spl42_24])],[avatar_definition]) ).
fof(f533,plain,
( ! [X0] :
( leq(s(zero),sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(nbr_proc)) )
| ~ spl42_24 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f535,definition,
( spl42_25
<=> sP40(index(elid,nbr_proc)) ),
introduced(definition,[new_symbols(definition,[spl42_25])],[avatar_definition]) ).
fof(f538,plain,
( spl42_24
| spl42_25 ),
inference(avatar_split_clause,[],[f529,f535,f532]) ).
fof(f569,definition,
( spl42_31
<=> sP34(index(elid,nbr_proc)) ),
introduced(definition,[new_symbols(definition,[spl42_31])],[avatar_definition]) ).
fof(f570,plain,
( ~ sP34(index(elid,nbr_proc))
| spl42_31 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f576,plain,
! [X0] :
( host(X0) != nbr_proc
| sP18(nbr_proc)
| sP19(index(status,nbr_proc))
| ~ sP34(sK2)
| sP35(X0) ),
inference(superposition,[],[f220,f257]) ).
fof(f595,plain,
! [X0] :
( host(X0) != nbr_proc
| sP19(index(status,nbr_proc))
| ~ sP34(sK2)
| sP35(X0) ),
inference(forward_subsumption_resolution,[],[f576,f181]) ).
fof(f606,plain,
! [X0] :
( sP19(elec_1)
| host(X0) != nbr_proc
| ~ sP34(sK2)
| sP35(X0) ),
inference(forward_demodulation,[],[f595,f271]) ).
fof(f611,plain,
! [X0] :
( host(X0) != nbr_proc
| ~ sP34(sK2)
| sP35(X0) ),
inference(forward_subsumption_resolution,[],[f606,f182]) ).
fof(f615,plain,
! [X0] :
( ~ sP34(index(elid,nbr_proc))
| host(X0) != nbr_proc
| sP35(X0) ),
inference(forward_demodulation,[],[f611,f411]) ).
fof(f620,definition,
( spl42_35
<=> ! [X0] :
( host(X0) != nbr_proc
| sP35(X0) ) ),
introduced(definition,[new_symbols(definition,[spl42_35])],[avatar_definition]) ).
fof(f621,plain,
( ! [X0] :
( host(X0) != nbr_proc
| sP35(X0) )
| ~ spl42_35 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f622,plain,
( spl42_35
| ~ spl42_31 ),
inference(avatar_split_clause,[],[f615,f569,f620]) ).
fof(f635,plain,
! [X0] :
( host(X0) != host(sK2)
| sP20(host(X0))
| sP21(index(status,host(X0)))
| ~ sP36(X0)
| sP37(sK5) ),
inference(superposition,[],[f224,f248]) ).
fof(f637,plain,
! [X0] :
( host(X0) != host(sK2)
| sP20(host(X0))
| sP21(index(status,host(X0)))
| ~ sP36(X0) ),
inference(forward_subsumption_resolution,[],[f635,f341]) ).
fof(f644,definition,
( spl42_37
<=> ! [X0] :
( host(X0) != nbr_proc
| ~ sP36(X0)
| sP21(index(status,host(X0)))
| sP20(host(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl42_37])],[avatar_definition]) ).
fof(f645,plain,
( ! [X0] :
( host(X0) != nbr_proc
| ~ sP36(X0)
| sP21(index(status,host(X0)))
| sP20(host(X0)) )
| ~ spl42_37 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f652,plain,
! [X0] :
( host(X0) != nbr_proc
| sP20(host(X0))
| sP21(index(status,host(X0)))
| ~ sP36(X0) ),
inference(forward_demodulation,[],[f637,f257]) ).
fof(f663,plain,
spl42_37,
inference(avatar_split_clause,[],[f652,f644]) ).
fof(f681,definition,
( spl42_41
<=> sP36(index(elid,nbr_proc)) ),
introduced(definition,[new_symbols(definition,[spl42_41])],[avatar_definition]) ).
fof(f682,plain,
( sP36(index(elid,nbr_proc))
| ~ spl42_41 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f683,plain,
( ~ sP36(index(elid,nbr_proc))
| spl42_41 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f694,plain,
! [X0] :
( host(X0) != nbr_proc
| sP22(nbr_proc)
| sP23(index(status,nbr_proc))
| ~ sP38(sK2)
| sP39(X0) ),
inference(superposition,[],[f228,f257]) ).
fof(f713,plain,
! [X0] :
( host(X0) != nbr_proc
| sP23(index(status,nbr_proc))
| ~ sP38(sK2)
| sP39(X0) ),
inference(forward_subsumption_resolution,[],[f694,f187]) ).
fof(f724,plain,
! [X0] :
( sP23(elec_1)
| host(X0) != nbr_proc
| ~ sP38(sK2)
| sP39(X0) ),
inference(forward_demodulation,[],[f713,f271]) ).
fof(f729,plain,
! [X0] :
( host(X0) != nbr_proc
| ~ sP38(sK2)
| sP39(X0) ),
inference(forward_subsumption_resolution,[],[f724,f188]) ).
fof(f733,plain,
! [X0] :
( ~ sP38(index(elid,nbr_proc))
| host(X0) != nbr_proc
| sP39(X0) ),
inference(forward_demodulation,[],[f729,f411]) ).
fof(f738,definition,
( spl42_46
<=> ! [X0] :
( host(X0) != nbr_proc
| sP39(X0) ) ),
introduced(definition,[new_symbols(definition,[spl42_46])],[avatar_definition]) ).
fof(f739,plain,
( ! [X0] :
( host(X0) != nbr_proc
| sP39(X0) )
| ~ spl42_46 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f740,plain,
( spl42_46
| ~ spl42_17 ),
inference(avatar_split_clause,[],[f733,f491,f738]) ).
fof(f748,plain,
! [X0] :
( host(X0) != nbr_proc
| sP24(nbr_proc)
| sP25(index(status,nbr_proc))
| ~ sP40(sK2)
| sP41(X0) ),
inference(superposition,[],[f232,f257]) ).
fof(f767,plain,
! [X0] :
( host(X0) != nbr_proc
| sP25(index(status,nbr_proc))
| ~ sP40(sK2)
| sP41(X0) ),
inference(forward_subsumption_resolution,[],[f748,f190]) ).
fof(f778,plain,
! [X0] :
( sP25(elec_1)
| host(X0) != nbr_proc
| ~ sP40(sK2)
| sP41(X0) ),
inference(forward_demodulation,[],[f767,f271]) ).
fof(f783,plain,
! [X0] :
( host(X0) != nbr_proc
| ~ sP40(sK2)
| sP41(X0) ),
inference(forward_subsumption_resolution,[],[f778,f191]) ).
fof(f787,plain,
! [X0] :
( ~ sP40(index(elid,nbr_proc))
| host(X0) != nbr_proc
| sP41(X0) ),
inference(forward_demodulation,[],[f783,f411]) ).
fof(f792,definition,
( spl42_50
<=> ! [X0] :
( host(X0) != nbr_proc
| sP41(X0) ) ),
introduced(definition,[new_symbols(definition,[spl42_50])],[avatar_definition]) ).
fof(f793,plain,
( ! [X0] :
( host(X0) != nbr_proc
| sP41(X0) )
| ~ spl42_50 ),
inference(avatar_component_clause,[],[f792]) ).
fof(f794,plain,
( spl42_50
| ~ spl42_25 ),
inference(avatar_split_clause,[],[f787,f535,f792]) ).
fof(f800,plain,
! [X0] :
( leq(host(sK2),sK8(X0,sK2))
| host(sK6) = sK8(X0,sK2)
| ~ leq(s(zero),sK8(X0,sK2))
| ~ elem(m_Down(X0),queue(host(sK2)))
| sP34(sK2) ),
inference(resolution,[],[f250,f218]) ).
fof(f804,plain,
! [X0] :
( leq(host(index(elid,nbr_proc)),sK8(X0,index(elid,nbr_proc)))
| host(sK6) = sK8(X0,sK2)
| ~ leq(s(zero),sK8(X0,sK2))
| ~ elem(m_Down(X0),queue(host(sK2)))
| sP34(sK2) ),
inference(forward_demodulation,[],[f800,f411]) ).
fof(f806,plain,
! [X0] :
( leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| host(sK6) = sK8(X0,sK2)
| ~ leq(s(zero),sK8(X0,sK2))
| ~ elem(m_Down(X0),queue(host(sK2)))
| sP34(sK2) ),
inference(forward_demodulation,[],[f804,f456]) ).
fof(f807,plain,
! [X0] :
( host(sK6) = sK8(X0,index(elid,nbr_proc))
| leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| ~ leq(s(zero),sK8(X0,sK2))
| ~ elem(m_Down(X0),queue(host(sK2)))
| sP34(sK2) ),
inference(forward_demodulation,[],[f806,f411]) ).
fof(f808,plain,
! [X0] :
( ~ leq(s(zero),sK8(X0,index(elid,nbr_proc)))
| host(sK6) = sK8(X0,index(elid,nbr_proc))
| leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| ~ elem(m_Down(X0),queue(host(sK2)))
| sP34(sK2) ),
inference(forward_demodulation,[],[f807,f411]) ).
fof(f809,plain,
! [X0] :
( ~ elem(m_Down(X0),queue(nbr_proc))
| ~ leq(s(zero),sK8(X0,index(elid,nbr_proc)))
| host(sK6) = sK8(X0,index(elid,nbr_proc))
| leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| sP34(sK2) ),
inference(forward_demodulation,[],[f808,f257]) ).
fof(f810,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(nbr_proc))
| host(sK6) = sK8(X0,index(elid,nbr_proc))
| leq(nbr_proc,sK8(X0,index(elid,nbr_proc)))
| sP34(sK2) )
| ~ spl42_24 ),
inference(forward_subsumption_resolution,[],[f809,f533]) ).
fof(f811,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(nbr_proc))
| host(sK6) = sK8(X0,index(elid,nbr_proc))
| sP34(sK2) )
| ~ spl42_16
| ~ spl42_24 ),
inference(forward_subsumption_resolution,[],[f810,f489]) ).
fof(f812,plain,
( ! [X0] :
( sP34(index(elid,nbr_proc))
| ~ elem(m_Down(X0),queue(nbr_proc))
| host(sK6) = sK8(X0,index(elid,nbr_proc)) )
| ~ spl42_16
| ~ spl42_24 ),
inference(forward_demodulation,[],[f811,f411]) ).
fof(f813,plain,
( ! [X0] :
( host(sK6) = sK8(X0,index(elid,nbr_proc))
| ~ elem(m_Down(X0),queue(nbr_proc)) )
| ~ spl42_16
| ~ spl42_24
| spl42_31 ),
inference(forward_subsumption_resolution,[],[f812,f570]) ).
fof(f1197,plain,
( ! [X0] :
( host(X0) != host(sK6)
| ~ elem(m_Down(X0),queue(host(index(elid,nbr_proc))))
| sP36(index(elid,nbr_proc))
| ~ elem(m_Down(X0),queue(nbr_proc)) )
| ~ spl42_16
| ~ spl42_24
| spl42_31 ),
inference(superposition,[],[f222,f813]) ).
fof(f1198,plain,
( ! [X0] :
( host(X0) != host(sK6)
| ~ elem(m_Down(X0),queue(host(index(elid,nbr_proc))))
| ~ elem(m_Down(X0),queue(nbr_proc)) )
| ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(forward_subsumption_resolution,[],[f1197,f683]) ).
fof(f1337,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(nbr_proc))
| host(X0) != host(sK6)
| ~ elem(m_Down(X0),queue(nbr_proc)) )
| ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(forward_demodulation,[],[f1198,f456]) ).
fof(f1338,plain,
( ! [X0] :
( host(X0) != host(sK6)
| ~ elem(m_Down(X0),queue(nbr_proc)) )
| ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(duplicate_literal_removal,[],[f1337]) ).
fof(f1438,plain,
( nbr_proc != nbr_proc
| ~ sP36(index(elid,nbr_proc))
| sP21(index(status,nbr_proc))
| sP20(nbr_proc)
| ~ spl42_37 ),
inference(superposition,[],[f645,f456]) ).
fof(f1445,plain,
( ~ sP36(index(elid,nbr_proc))
| sP21(index(status,nbr_proc))
| sP20(nbr_proc)
| ~ spl42_37 ),
inference(trivial_inequality_removal,[],[f1438]) ).
fof(f1664,plain,
( nbr_proc != host(sK2)
| sP35(sK5)
| ~ spl42_35 ),
inference(superposition,[],[f621,f248]) ).
fof(f1673,plain,
( sP35(sK5)
| ~ spl42_35 ),
inference(forward_subsumption_resolution,[],[f1664,f257]) ).
fof(f1675,plain,
( $false
| ~ spl42_35 ),
inference(forward_subsumption_resolution,[],[f1673,f321]) ).
fof(f1676,plain,
~ spl42_35,
inference(avatar_contradiction_clause,[],[f1675]) ).
fof(f1679,plain,
( nbr_proc != host(sK2)
| sP39(sK5)
| ~ spl42_46 ),
inference(superposition,[],[f739,f248]) ).
fof(f1688,plain,
( sP39(sK5)
| ~ spl42_46 ),
inference(forward_subsumption_resolution,[],[f1679,f257]) ).
fof(f1690,plain,
( $false
| ~ spl42_46 ),
inference(forward_subsumption_resolution,[],[f1688,f357]) ).
fof(f1691,plain,
~ spl42_46,
inference(avatar_contradiction_clause,[],[f1690]) ).
fof(f1694,plain,
( nbr_proc != host(sK2)
| sP41(sK5)
| ~ spl42_50 ),
inference(superposition,[],[f793,f248]) ).
fof(f1703,plain,
( sP41(sK5)
| ~ spl42_50 ),
inference(forward_subsumption_resolution,[],[f1694,f257]) ).
fof(f1705,plain,
( $false
| ~ spl42_50 ),
inference(forward_subsumption_resolution,[],[f1703,f373]) ).
fof(f1706,plain,
~ spl42_50,
inference(avatar_contradiction_clause,[],[f1705]) ).
fof(f1831,plain,
( ~ elem(m_Down(sK6),queue(nbr_proc))
| ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(equality_resolution,[],[f1338]) ).
fof(f1833,plain,
( ~ elem(m_Down(sK6),sK0)
| ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(resolution,[],[f1831,f276]) ).
fof(f1834,plain,
( $false
| ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(forward_subsumption_resolution,[],[f1833,f114]) ).
fof(f1835,plain,
( ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(avatar_contradiction_clause,[],[f1834]) ).
fof(f1839,plain,
( sP21(index(status,nbr_proc))
| sP20(nbr_proc)
| ~ spl42_37
| ~ spl42_41 ),
inference(forward_subsumption_resolution,[],[f1445,f682]) ).
fof(f1844,plain,
( sP21(index(status,nbr_proc))
| ~ spl42_37
| ~ spl42_41 ),
inference(forward_subsumption_resolution,[],[f1839,f184]) ).
fof(f1848,plain,
( sP21(elec_1)
| ~ spl42_37
| ~ spl42_41 ),
inference(forward_demodulation,[],[f1844,f271]) ).
fof(f1852,plain,
( $false
| ~ spl42_37
| ~ spl42_41 ),
inference(forward_subsumption_resolution,[],[f1848,f185]) ).
fof(f1853,plain,
( ~ spl42_37
| ~ spl42_41 ),
inference(avatar_contradiction_clause,[],[f1852]) ).
cnf(s26,plain,
( spl42_16
| spl42_17 ),
inference(sat_conversion,[],[f494]) ).
cnf(s32,plain,
( spl42_24
| spl42_25 ),
inference(sat_conversion,[],[f538]) ).
cnf(s41,plain,
( ~ spl42_31
| spl42_35 ),
inference(sat_conversion,[],[f622]) ).
cnf(s48,plain,
spl42_37,
inference(sat_conversion,[],[f663]) ).
cnf(s57,plain,
( ~ spl42_17
| spl42_46 ),
inference(sat_conversion,[],[f740]) ).
cnf(s65,plain,
( ~ spl42_25
| spl42_50 ),
inference(sat_conversion,[],[f794]) ).
cnf(s123,plain,
~ spl42_35,
inference(sat_conversion,[],[f1676]) ).
cnf(s126,plain,
~ spl42_46,
inference(sat_conversion,[],[f1691]) ).
cnf(s129,plain,
~ spl42_50,
inference(sat_conversion,[],[f1706]) ).
cnf(s135,plain,
( ~ spl42_16
| ~ spl42_24
| spl42_31
| spl42_41 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s139,plain,
( ~ spl42_37
| ~ spl42_41 ),
inference(sat_conversion,[],[f1853]) ).
cnf(s143,plain,
~ spl42_25,
inference(rat,[],[s65,s129]) ).
cnf(s146,plain,
~ spl42_17,
inference(rat,[],[s57,s126]) ).
cnf(s147,plain,
~ spl42_41,
inference(rat,[],[s139,s48]) ).
cnf(s150,plain,
~ spl42_31,
inference(rat,[],[s41,s123]) ).
cnf(s154,plain,
spl42_24,
inference(rat,[],[s32,s143]) ).
cnf(s155,plain,
~ spl42_16,
inference(rat,[],[s135,s147,s150,s154]) ).
cnf(s159,plain,
$false,
inference(rat,[],[s26,s146,s155]) ).
fof(f1854,plain,
$false,
inference(avatar_sat_refutation,[],[s159]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV473+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n017.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:05:36 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.78/1.14 % (3480961)Detected formulas, will run a generic FOF schedule.
% 1.78/1.14 % (3481109)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=359456278:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.78/1.14 % (3481111)dis-21_1_sil=8000:lcm=predicate:random_seed=3104521721:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 1.78/1.14 % (3481106)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4053431918:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.78/1.14 % (3481105)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3314723447:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.78/1.14 % (3481107)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1432637968:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.78/1.14 % (3481104)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4160872931:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.78/1.14 % (3481109)Instruction limit reached!
% 1.78/1.14 % (3481109)------------------------------
% 1.78/1.14 % (3481109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.78/1.14 % (3481109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.78/1.14 % (3481109)CaDiCaL version: 2.1.3
% 1.78/1.14 % (3481109)Termination reason: Instruction limit
% 1.78/1.14 % (3481109)Termination phase: Saturation
% 1.78/1.14 % (3481109)Time elapsed: 0.056 s
% 1.78/1.14 % (3481109)Peak memory usage: 90 MB
% 1.78/1.14 % (3481109)Instructions burned: 141 (million)
% 1.78/1.14 % (3481107)First to succeed.
% 1.78/1.14 % (3481107)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3480961"
% 1.78/1.14 % (3481108)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3994299769:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.78/1.14 % (3481111)Instruction limit reached!
% 1.78/1.14 % (3481111)------------------------------
% 1.78/1.14 % (3481111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.78/1.14 % (3481111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.78/1.14 % (3481111)CaDiCaL version: 2.1.3
% 1.78/1.14 % (3481111)Termination reason: Instruction limit
% 1.78/1.14 % (3481111)Termination phase: Saturation
% 1.78/1.14 % (3481111)Time elapsed: 0.078 s
% 1.78/1.14 % (3481111)Peak memory usage: 89 MB
% 1.78/1.14 % (3481111)Instructions burned: 129 (million)
% 1.78/1.14 % (3481108)Instruction limit reached!
% 1.78/1.14 % (3481108)------------------------------
% 1.78/1.14 % (3481108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.78/1.14 % (3481108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.78/1.14 % (3481108)CaDiCaL version: 2.1.3
% 1.78/1.14 % (3481108)Termination reason: Instruction limit
% 1.78/1.14 % (3481108)Termination phase: Saturation
% 1.78/1.14 % (3481108)Time elapsed: 0.075 s
% 1.78/1.14 % (3481108)Peak memory usage: 88 MB
% 1.78/1.14 % (3481108)Instructions burned: 119 (million)
% 1.78/1.14 % (3481138)lrs+10_1_sil=8000:sp=occurrence:random_seed=1920848250:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 1.78/1.14 % (3481138)Also succeeded, but the first one will report.
% 1.78/1.14 % (3481149)lrs+10_1_sil=32000:urr=on:br=off:random_seed=912818585:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 1.78/1.14 % (3481149)Also succeeded, but the first one will report.
% 1.78/1.14 % (3481175)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2388225670:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 1.78/1.14 % (3481107)Refutation found. Thanks to Tanya!
% 1.78/1.14 % SZS status Theorem for theBenchmark
% 1.78/1.14 % SZS output start Proof for theBenchmark
% See solution above
% 4.00/1.33 % (3481107)------------------------------
% 4.00/1.33 % (3481107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.00/1.33 % (3481107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/1.33 % (3481107)CaDiCaL version: 2.1.3
% 4.00/1.33 % (3481107)Termination reason: Refutation
% 4.00/1.33 % (3481107)Time elapsed: 0.039 s
% 4.00/1.33 % (3481107)Peak memory usage: 90 MB
% 4.00/1.33 % (3481107)Instructions burned: 61 (million)
% 4.00/1.33 % (3481107)------------------------------
% 4.00/1.33 % (3481107)------------------------------
% 4.00/1.33 % (3480961)Success in time 0.466 s
% 4.00/1.33 % Vampire exiting
%------------------------------------------------------------------------------