%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV467+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 : n018.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:53 PM UTC 2026
% Result : Theorem 3.02s 1.12s
% Output : Refutation 3.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 30
% Syntax : Number of formulae : 197 ( 47 unt; 26 def)
% Number of atoms : 1252 ( 360 equ)
% Maximal formula atoms : 98 ( 6 avg)
% Number of connectives : 1777 ( 722 ~; 598 |; 356 &)
% ( 20 <=>; 81 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 31 ( 29 usr; 11 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 21 con; 0-2 aty)
% Number of variables : 461 ( 2 sgn 434 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0] : leq(host(X0),nbr_proc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_04) ).
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(f62,axiom,
! [X0,X1] :
( ( leq(X0,X1)
& leq(X1,X0) )
<=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_61) ).
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] :
( elem(m_Halt(X5),queue(host(X4)))
=> ~ leq(host(X4),host(X5)) )
& ! [X4,X6,X5] :
( elem(m_Ack(X5,X4),queue(host(X6)))
=> ~ leq(host(X4),host(X5)) )
& ! [X4,X5] :
( ( X5 != X4
& host(X5) = host(X4) )
=> ( ~ setIn(X4,alive)
| ~ setIn(X5,alive) ) )
& ! [X4,X5] :
( ( setIn(X5,alive)
& elem(m_Ack(X5,X4),queue(host(X5))) )
=> leq(host(X4),index(pendack,host(X5))) )
& ! [X4,X5] :
( ( setIn(X5,alive)
& index(status,host(X5)) = elec_1 )
=> ~ elem(m_Ack(X5,X4),queue(host(X5))) )
& ! [X4] :
( ( ( index(status,host(X4)) = elec_1
| index(status,host(X4)) = elec_2 )
& setIn(X4,alive) )
=> index(elid,host(X4)) = X4 )
& ! [X4,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Down(X6),queue(host(X5)))
& host(X6) = host(X4) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [X4,X5] :
( ( ~ leq(host(X4),host(X5))
& setIn(X4,alive)
& setIn(X5,alive)
& index(status,host(X4)) = elec_2
& index(status,host(X5)) = elec_2 )
=> leq(index(pendack,host(X5)),host(X4)) )
& ! [X4,X6,X5] :
( ( setIn(X4,alive)
& setIn(X5,alive)
& host(X5) = host(X6)
& index(status,host(X4)) = elec_2
& index(status,host(X5)) = elec_2 )
=> ~ elem(m_Ack(X4,X6),queue(host(X4))) )
& ! [X4,X5] :
( ( ~ leq(host(X4),host(X5))
& setIn(X4,alive)
& setIn(X5,alive)
& index(status,host(X4)) = elec_2
& index(status,host(X5)) = elec_2 )
=> ~ leq(index(pendack,host(X4)),index(pendack,host(X5))) )
& ! [X4,X6,X5] :
( ( ~ leq(index(pendack,host(X5)),host(X4))
& setIn(X5,alive)
& elem(m_Halt(X5),queue(host(X6)))
& index(status,host(X5)) = elec_2 )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [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))) ) )
& ! [X4,X7,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Down(X6),queue(host(X5)))
& elem(m_Ack(X5,X7),queue(host(X5)))
& leq(nbr_proc,s(index(pendack,host(X5))))
& index(status,host(X5)) = elec_2
& host(X7) = index(pendack,host(X5))
& host(X6) = s(index(pendack,host(X5))) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& queue(host(X2)) = cons(m_Down(X3),X0) )
=> ( setIn(X2,alive)
=> ( ~ leq(host(X2),host(X3))
=> ( ~ ( ( index(ldr,host(X2)) = host(X3)
& index(status,host(X2)) = norm )
| ( index(status,host(X2)) = wait
& host(X3) = host(index(elid,host(X2))) ) )
=> ( ( ! [X4] :
( ( ~ leq(host(X2),X4)
& leq(s(zero),X4) )
=> ( setIn(X4,index(down,host(X2)))
| X4 = host(X3) ) )
& index(status,host(X2)) = elec_1 )
=> ( leq(nbr_proc,host(X2))
=> ! [X4] :
( ~ setIn(host(X4),setEmpty)
=> ! [X8] :
( host(X2) = host(X8)
=> ! [X9,X10,X11] :
( host(X2) != host(X11)
=> ( ( setIn(X11,alive)
& elem(m_Down(X10),queue(host(X11)))
& elem(m_Ack(X11,X9),queue(host(X11)))
& leq(nbr_proc,s(index(pendack,host(X11))))
& index(status,host(X11)) = elec_2
& host(X9) = index(pendack,host(X11))
& host(X10) = s(index(pendack,host(X11))) )
=> ~ ( setIn(X8,alive)
& host(X2) = host(X8) ) ) ) ) ) ) ) ) ) ) ),
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] :
( elem(m_Halt(X5),queue(host(X4)))
=> ~ leq(host(X4),host(X5)) )
& ! [X4,X6,X5] :
( elem(m_Ack(X5,X4),queue(host(X6)))
=> ~ leq(host(X4),host(X5)) )
& ! [X4,X5] :
( ( X5 != X4
& host(X5) = host(X4) )
=> ( ~ setIn(X4,alive)
| ~ setIn(X5,alive) ) )
& ! [X4,X5] :
( ( setIn(X5,alive)
& elem(m_Ack(X5,X4),queue(host(X5))) )
=> leq(host(X4),index(pendack,host(X5))) )
& ! [X4,X5] :
( ( setIn(X5,alive)
& index(status,host(X5)) = elec_1 )
=> ~ elem(m_Ack(X5,X4),queue(host(X5))) )
& ! [X4] :
( ( ( index(status,host(X4)) = elec_1
| index(status,host(X4)) = elec_2 )
& setIn(X4,alive) )
=> index(elid,host(X4)) = X4 )
& ! [X4,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Down(X6),queue(host(X5)))
& host(X6) = host(X4) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [X4,X5] :
( ( ~ leq(host(X4),host(X5))
& setIn(X4,alive)
& setIn(X5,alive)
& index(status,host(X4)) = elec_2
& index(status,host(X5)) = elec_2 )
=> leq(index(pendack,host(X5)),host(X4)) )
& ! [X4,X6,X5] :
( ( setIn(X4,alive)
& setIn(X5,alive)
& host(X5) = host(X6)
& index(status,host(X4)) = elec_2
& index(status,host(X5)) = elec_2 )
=> ~ elem(m_Ack(X4,X6),queue(host(X4))) )
& ! [X4,X5] :
( ( ~ leq(host(X4),host(X5))
& setIn(X4,alive)
& setIn(X5,alive)
& index(status,host(X4)) = elec_2
& index(status,host(X5)) = elec_2 )
=> ~ leq(index(pendack,host(X4)),index(pendack,host(X5))) )
& ! [X4,X6,X5] :
( ( ~ leq(index(pendack,host(X5)),host(X4))
& setIn(X5,alive)
& elem(m_Halt(X5),queue(host(X6)))
& index(status,host(X5)) = elec_2 )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [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))) ) )
& ! [X4,X7,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Down(X6),queue(host(X5)))
& elem(m_Ack(X5,X7),queue(host(X5)))
& leq(nbr_proc,s(index(pendack,host(X5))))
& index(status,host(X5)) = elec_2
& host(X7) = index(pendack,host(X5))
& host(X6) = s(index(pendack,host(X5))) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& queue(host(X2)) = cons(m_Down(X3),X0) )
=> ( setIn(X2,alive)
=> ( ~ leq(host(X2),host(X3))
=> ( ~ ( ( index(ldr,host(X2)) = host(X3)
& index(status,host(X2)) = norm )
| ( index(status,host(X2)) = wait
& host(X3) = host(index(elid,host(X2))) ) )
=> ( ( ! [X4] :
( ( ~ leq(host(X2),X4)
& leq(s(zero),X4) )
=> ( setIn(X4,index(down,host(X2)))
| X4 = host(X3) ) )
& index(status,host(X2)) = elec_1 )
=> ( leq(nbr_proc,host(X2))
=> ! [X4] :
( ~ setIn(host(X4),setEmpty)
=> ! [X8] :
( host(X2) = host(X8)
=> ! [X9,X10,X11] :
( host(X2) != host(X11)
=> ( ( setIn(X11,alive)
& elem(m_Down(X10),queue(host(X11)))
& elem(m_Ack(X11,X9),queue(host(X11)))
& leq(nbr_proc,s(index(pendack,host(X11))))
& index(status,host(X11)) = elec_2
& host(X9) = index(pendack,host(X11))
& host(X10) = s(index(pendack,host(X11))) )
=> ~ ( setIn(X8,alive)
& host(X2) = host(X8) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f67]) ).
fof(f69,plain,
~ ! [X0,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] :
( elem(m_Halt(X9),queue(host(X8)))
=> ~ leq(host(X8),host(X9)) )
& ! [X10,X11,X12] :
( elem(m_Ack(X12,X10),queue(host(X11)))
=> ~ leq(host(X10),host(X12)) )
& ! [X13,X14] :
( ( X13 != X14
& host(X13) = host(X14) )
=> ( ~ setIn(X13,alive)
| ~ setIn(X14,alive) ) )
& ! [X15,X16] :
( ( setIn(X16,alive)
& elem(m_Ack(X16,X15),queue(host(X16))) )
=> leq(host(X15),index(pendack,host(X16))) )
& ! [X17,X18] :
( ( setIn(X18,alive)
& elec_1 = index(status,host(X18)) )
=> ~ elem(m_Ack(X18,X17),queue(host(X18))) )
& ! [X19] :
( ( ( elec_1 = index(status,host(X19))
| elec_2 = index(status,host(X19)) )
& setIn(X19,alive) )
=> index(elid,host(X19)) = X19 )
& ! [X20,X21,X22] :
( ( setIn(X22,alive)
& elem(m_Down(X21),queue(host(X22)))
& host(X20) = host(X21) )
=> ~ ( setIn(X20,alive)
& host(X20) = index(ldr,host(X20))
& norm = index(status,host(X20)) ) )
& ! [X23,X24] :
( ( ~ leq(host(X23),host(X24))
& setIn(X23,alive)
& setIn(X24,alive)
& elec_2 = index(status,host(X23))
& elec_2 = index(status,host(X24)) )
=> leq(index(pendack,host(X24)),host(X23)) )
& ! [X25,X26,X27] :
( ( setIn(X25,alive)
& setIn(X27,alive)
& host(X27) = host(X26)
& elec_2 = index(status,host(X25))
& elec_2 = index(status,host(X27)) )
=> ~ elem(m_Ack(X25,X26),queue(host(X25))) )
& ! [X28,X29] :
( ( ~ leq(host(X28),host(X29))
& setIn(X28,alive)
& setIn(X29,alive)
& elec_2 = index(status,host(X28))
& elec_2 = index(status,host(X29)) )
=> ~ leq(index(pendack,host(X28)),index(pendack,host(X29))) )
& ! [X30,X31,X32] :
( ( ~ leq(index(pendack,host(X32)),host(X30))
& setIn(X32,alive)
& elem(m_Halt(X32),queue(host(X31)))
& elec_2 = index(status,host(X32)) )
=> ~ ( setIn(X30,alive)
& host(X30) = index(ldr,host(X30))
& norm = index(status,host(X30)) ) )
& ! [X33,X34,X35,X36] :
( ( ! [X37] :
( ( ~ leq(host(X36),X37)
& leq(s(zero),X37) )
=> ( setIn(X37,index(down,host(X36)))
| host(X35) = X37 ) )
& elem(m_Down(X35),queue(host(X36)))
& nbr_proc = host(X36)
& host(X36) = host(X34)
& elec_1 = index(status,host(X36)) )
=> ~ ( setIn(X33,alive)
& elem(m_Down(X34),queue(host(X33))) ) )
& ! [X38,X39,X40,X41] :
( ( setIn(X41,alive)
& elem(m_Down(X40),queue(host(X41)))
& elem(m_Ack(X41,X39),queue(host(X41)))
& leq(nbr_proc,s(index(pendack,host(X41))))
& elec_2 = index(status,host(X41))
& index(pendack,host(X41)) = host(X39)
& s(index(pendack,host(X41))) = host(X40) )
=> ~ ( setIn(X38,alive)
& host(X38) = index(ldr,host(X38))
& norm = index(status,host(X38)) ) )
& queue(host(X2)) = cons(m_Down(X3),X0) )
=> ( setIn(X2,alive)
=> ( ~ leq(host(X2),host(X3))
=> ( ~ ( ( index(ldr,host(X2)) = host(X3)
& index(status,host(X2)) = norm )
| ( index(status,host(X2)) = wait
& host(X3) = host(index(elid,host(X2))) ) )
=> ( ( ! [X42] :
( ( ~ leq(host(X2),X42)
& leq(s(zero),X42) )
=> ( setIn(X42,index(down,host(X2)))
| host(X3) = X42 ) )
& index(status,host(X2)) = elec_1 )
=> ( leq(nbr_proc,host(X2))
=> ! [X43] :
( ~ setIn(host(X43),setEmpty)
=> ! [X44] :
( host(X2) = host(X44)
=> ! [X45,X46,X47] :
( host(X2) != host(X47)
=> ( ( setIn(X47,alive)
& elem(m_Down(X46),queue(host(X47)))
& elem(m_Ack(X47,X45),queue(host(X47)))
& leq(nbr_proc,s(index(pendack,host(X47))))
& elec_2 = index(status,host(X47))
& index(pendack,host(X47)) = host(X45)
& s(index(pendack,host(X47))) = host(X46) )
=> ~ ( setIn(X44,alive)
& host(X2) = host(X44) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f68]) ).
fof(f70,plain,
? [X0,X2,X3] :
( ? [X43] :
( ? [X44] :
( ? [X45,X46,X47] :
( setIn(X44,alive)
& host(X2) = host(X44)
& setIn(X47,alive)
& elem(m_Down(X46),queue(host(X47)))
& elem(m_Ack(X47,X45),queue(host(X47)))
& leq(nbr_proc,s(index(pendack,host(X47))))
& elec_2 = index(status,host(X47))
& index(pendack,host(X47)) = host(X45)
& s(index(pendack,host(X47))) = host(X46)
& host(X2) != host(X47) )
& host(X2) = host(X44) )
& ~ setIn(host(X43),setEmpty) )
& leq(nbr_proc,host(X2))
& ! [X42] :
( setIn(X42,index(down,host(X2)))
| host(X3) = X42
| leq(host(X2),X42)
| ~ leq(s(zero),X42) )
& index(status,host(X2)) = elec_1
& ( host(X3) != index(ldr,host(X2))
| norm != index(status,host(X2)) )
& ( wait != index(status,host(X2))
| host(X3) != host(index(elid,host(X2))) )
& ~ leq(host(X2),host(X3))
& 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] :
( ~ leq(host(X8),host(X9))
| ~ elem(m_Halt(X9),queue(host(X8))) )
& ! [X10,X11,X12] :
( ~ leq(host(X10),host(X12))
| ~ elem(m_Ack(X12,X10),queue(host(X11))) )
& ! [X13,X14] :
( ~ setIn(X13,alive)
| ~ setIn(X14,alive)
| X13 = X14
| host(X13) != host(X14) )
& ! [X15,X16] :
( leq(host(X15),index(pendack,host(X16)))
| ~ setIn(X16,alive)
| ~ elem(m_Ack(X16,X15),queue(host(X16))) )
& ! [X17,X18] :
( ~ elem(m_Ack(X18,X17),queue(host(X18)))
| ~ setIn(X18,alive)
| elec_1 != index(status,host(X18)) )
& ! [X19] :
( index(elid,host(X19)) = X19
| ( elec_1 != index(status,host(X19))
& elec_2 != index(status,host(X19)) )
| ~ setIn(X19,alive) )
& ! [X20,X21,X22] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| ~ setIn(X22,alive)
| ~ elem(m_Down(X21),queue(host(X22)))
| host(X20) != host(X21) )
& ! [X23,X24] :
( leq(index(pendack,host(X24)),host(X23))
| leq(host(X23),host(X24))
| ~ setIn(X23,alive)
| ~ setIn(X24,alive)
| elec_2 != index(status,host(X23))
| elec_2 != index(status,host(X24)) )
& ! [X25,X26,X27] :
( ~ elem(m_Ack(X25,X26),queue(host(X25)))
| ~ setIn(X25,alive)
| ~ setIn(X27,alive)
| host(X27) != host(X26)
| elec_2 != index(status,host(X25))
| elec_2 != index(status,host(X27)) )
& ! [X28,X29] :
( ~ leq(index(pendack,host(X28)),index(pendack,host(X29)))
| leq(host(X28),host(X29))
| ~ setIn(X28,alive)
| ~ setIn(X29,alive)
| elec_2 != index(status,host(X28))
| elec_2 != index(status,host(X29)) )
& ! [X30,X31,X32] :
( ~ setIn(X30,alive)
| host(X30) != index(ldr,host(X30))
| norm != index(status,host(X30))
| leq(index(pendack,host(X32)),host(X30))
| ~ setIn(X32,alive)
| ~ elem(m_Halt(X32),queue(host(X31)))
| elec_2 != index(status,host(X32)) )
& ! [X33,X34,X35,X36] :
( ~ setIn(X33,alive)
| ~ elem(m_Down(X34),queue(host(X33)))
| ? [X37] :
( ~ setIn(X37,index(down,host(X36)))
& host(X35) != X37
& ~ leq(host(X36),X37)
& leq(s(zero),X37) )
| ~ elem(m_Down(X35),queue(host(X36)))
| nbr_proc != host(X36)
| host(X36) != host(X34)
| elec_1 != index(status,host(X36)) )
& ! [X38,X39,X40,X41] :
( ~ setIn(X38,alive)
| host(X38) != index(ldr,host(X38))
| norm != index(status,host(X38))
| ~ setIn(X41,alive)
| ~ elem(m_Down(X40),queue(host(X41)))
| ~ elem(m_Ack(X41,X39),queue(host(X41)))
| ~ leq(nbr_proc,s(index(pendack,host(X41))))
| elec_2 != index(status,host(X41))
| index(pendack,host(X41)) != host(X39)
| s(index(pendack,host(X41))) != host(X40) )
& queue(host(X2)) = cons(m_Down(X3),X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f71,plain,
? [X0,X2,X3] :
( ? [X43] :
( ? [X44] :
( ? [X45,X46,X47] :
( setIn(X44,alive)
& host(X2) = host(X44)
& setIn(X47,alive)
& elem(m_Down(X46),queue(host(X47)))
& elem(m_Ack(X47,X45),queue(host(X47)))
& leq(nbr_proc,s(index(pendack,host(X47))))
& elec_2 = index(status,host(X47))
& index(pendack,host(X47)) = host(X45)
& s(index(pendack,host(X47))) = host(X46)
& host(X2) != host(X47) )
& host(X2) = host(X44) )
& ~ setIn(host(X43),setEmpty) )
& leq(nbr_proc,host(X2))
& ! [X42] :
( setIn(X42,index(down,host(X2)))
| host(X3) = X42
| leq(host(X2),X42)
| ~ leq(s(zero),X42) )
& index(status,host(X2)) = elec_1
& ( host(X3) != index(ldr,host(X2))
| norm != index(status,host(X2)) )
& ( wait != index(status,host(X2))
| host(X3) != host(index(elid,host(X2))) )
& ~ leq(host(X2),host(X3))
& 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] :
( ~ leq(host(X8),host(X9))
| ~ elem(m_Halt(X9),queue(host(X8))) )
& ! [X10,X11,X12] :
( ~ leq(host(X10),host(X12))
| ~ elem(m_Ack(X12,X10),queue(host(X11))) )
& ! [X13,X14] :
( ~ setIn(X13,alive)
| ~ setIn(X14,alive)
| X13 = X14
| host(X13) != host(X14) )
& ! [X15,X16] :
( leq(host(X15),index(pendack,host(X16)))
| ~ setIn(X16,alive)
| ~ elem(m_Ack(X16,X15),queue(host(X16))) )
& ! [X17,X18] :
( ~ elem(m_Ack(X18,X17),queue(host(X18)))
| ~ setIn(X18,alive)
| elec_1 != index(status,host(X18)) )
& ! [X19] :
( index(elid,host(X19)) = X19
| ( elec_1 != index(status,host(X19))
& elec_2 != index(status,host(X19)) )
| ~ setIn(X19,alive) )
& ! [X20,X21,X22] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| ~ setIn(X22,alive)
| ~ elem(m_Down(X21),queue(host(X22)))
| host(X20) != host(X21) )
& ! [X23,X24] :
( leq(index(pendack,host(X24)),host(X23))
| leq(host(X23),host(X24))
| ~ setIn(X23,alive)
| ~ setIn(X24,alive)
| elec_2 != index(status,host(X23))
| elec_2 != index(status,host(X24)) )
& ! [X25,X26,X27] :
( ~ elem(m_Ack(X25,X26),queue(host(X25)))
| ~ setIn(X25,alive)
| ~ setIn(X27,alive)
| host(X27) != host(X26)
| elec_2 != index(status,host(X25))
| elec_2 != index(status,host(X27)) )
& ! [X28,X29] :
( ~ leq(index(pendack,host(X28)),index(pendack,host(X29)))
| leq(host(X28),host(X29))
| ~ setIn(X28,alive)
| ~ setIn(X29,alive)
| elec_2 != index(status,host(X28))
| elec_2 != index(status,host(X29)) )
& ! [X30,X31,X32] :
( ~ setIn(X30,alive)
| host(X30) != index(ldr,host(X30))
| norm != index(status,host(X30))
| leq(index(pendack,host(X32)),host(X30))
| ~ setIn(X32,alive)
| ~ elem(m_Halt(X32),queue(host(X31)))
| elec_2 != index(status,host(X32)) )
& ! [X33,X34,X35,X36] :
( ~ setIn(X33,alive)
| ~ elem(m_Down(X34),queue(host(X33)))
| ? [X37] :
( ~ setIn(X37,index(down,host(X36)))
& host(X35) != X37
& ~ leq(host(X36),X37)
& leq(s(zero),X37) )
| ~ elem(m_Down(X35),queue(host(X36)))
| nbr_proc != host(X36)
| host(X36) != host(X34)
| elec_1 != index(status,host(X36)) )
& ! [X38,X39,X40,X41] :
( ~ setIn(X38,alive)
| host(X38) != index(ldr,host(X38))
| norm != index(status,host(X38))
| ~ setIn(X41,alive)
| ~ elem(m_Down(X40),queue(host(X41)))
| ~ elem(m_Ack(X41,X39),queue(host(X41)))
| ~ leq(nbr_proc,s(index(pendack,host(X41))))
| elec_2 != index(status,host(X41))
| index(pendack,host(X41)) != host(X39)
| s(index(pendack,host(X41))) != host(X40) )
& queue(host(X2)) = cons(m_Down(X3),X0) ),
inference(flattening,[],[f70]) ).
fof(f78,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ? [X5,X6,X7] :
( setIn(X4,alive)
& host(X1) = host(X4)
& setIn(X7,alive)
& elem(m_Down(X6),queue(host(X7)))
& elem(m_Ack(X7,X5),queue(host(X7)))
& leq(nbr_proc,s(index(pendack,host(X7))))
& elec_2 = index(status,host(X7))
& host(X5) = index(pendack,host(X7))
& host(X6) = s(index(pendack,host(X7)))
& host(X1) != host(X7) )
& host(X1) = host(X4) )
& ~ setIn(host(X3),setEmpty) )
& leq(nbr_proc,host(X1))
& ! [X8] :
( setIn(X8,index(down,host(X1)))
| host(X2) = X8
| leq(host(X1),X8)
| ~ leq(s(zero),X8) )
& elec_1 = index(status,host(X1))
& ( host(X2) != index(ldr,host(X1))
| norm != index(status,host(X1)) )
& ( wait != index(status,host(X1))
| host(X2) != host(index(elid,host(X1))) )
& ~ leq(host(X1),host(X2))
& setIn(X1,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] :
( ~ leq(host(X13),host(X14))
| ~ elem(m_Halt(X14),queue(host(X13))) )
& ! [X15,X16,X17] :
( ~ leq(host(X15),host(X17))
| ~ elem(m_Ack(X17,X15),queue(host(X16))) )
& ! [X18,X19] :
( ~ setIn(X18,alive)
| ~ setIn(X19,alive)
| X18 = X19
| host(X18) != host(X19) )
& ! [X20,X21] :
( leq(host(X20),index(pendack,host(X21)))
| ~ setIn(X21,alive)
| ~ elem(m_Ack(X21,X20),queue(host(X21))) )
& ! [X22,X23] :
( ~ elem(m_Ack(X23,X22),queue(host(X23)))
| ~ setIn(X23,alive)
| elec_1 != index(status,host(X23)) )
& ! [X24] :
( index(elid,host(X24)) = X24
| ( elec_1 != index(status,host(X24))
& elec_2 != index(status,host(X24)) )
| ~ setIn(X24,alive) )
& ! [X25,X26,X27] :
( ~ setIn(X25,alive)
| host(X25) != index(ldr,host(X25))
| norm != index(status,host(X25))
| ~ setIn(X27,alive)
| ~ elem(m_Down(X26),queue(host(X27)))
| host(X26) != host(X25) )
& ! [X28,X29] :
( leq(index(pendack,host(X29)),host(X28))
| leq(host(X28),host(X29))
| ~ setIn(X28,alive)
| ~ setIn(X29,alive)
| elec_2 != index(status,host(X28))
| elec_2 != index(status,host(X29)) )
& ! [X30,X31,X32] :
( ~ elem(m_Ack(X30,X31),queue(host(X30)))
| ~ setIn(X30,alive)
| ~ setIn(X32,alive)
| host(X32) != host(X31)
| elec_2 != index(status,host(X30))
| elec_2 != index(status,host(X32)) )
& ! [X33,X34] :
( ~ leq(index(pendack,host(X33)),index(pendack,host(X34)))
| leq(host(X33),host(X34))
| ~ setIn(X33,alive)
| ~ setIn(X34,alive)
| elec_2 != index(status,host(X33))
| elec_2 != index(status,host(X34)) )
& ! [X35,X36,X37] :
( ~ setIn(X35,alive)
| host(X35) != index(ldr,host(X35))
| norm != index(status,host(X35))
| leq(index(pendack,host(X37)),host(X35))
| ~ setIn(X37,alive)
| ~ elem(m_Halt(X37),queue(host(X36)))
| elec_2 != index(status,host(X37)) )
& ! [X38,X39,X40,X41] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| ? [X42] :
( ~ setIn(X42,index(down,host(X41)))
& host(X40) != X42
& ~ leq(host(X41),X42)
& leq(s(zero),X42) )
| ~ elem(m_Down(X40),queue(host(X41)))
| nbr_proc != host(X41)
| host(X41) != host(X39)
| elec_1 != index(status,host(X41)) )
& ! [X43,X44,X45,X46] :
( ~ setIn(X43,alive)
| host(X43) != index(ldr,host(X43))
| norm != index(status,host(X43))
| ~ setIn(X46,alive)
| ~ elem(m_Down(X45),queue(host(X46)))
| ~ elem(m_Ack(X46,X44),queue(host(X46)))
| ~ leq(nbr_proc,s(index(pendack,host(X46))))
| elec_2 != index(status,host(X46))
| host(X44) != index(pendack,host(X46))
| host(X45) != s(index(pendack,host(X46))) )
& queue(host(X1)) = cons(m_Down(X2),X0) ),
inference(rectify,[],[f71]) ).
fof(f79,plain,
( setIn(sK4,alive)
& host(sK1) = host(sK4)
& setIn(sK7,alive)
& elem(m_Down(sK6),queue(host(sK7)))
& elem(m_Ack(sK7,sK5),queue(host(sK7)))
& leq(nbr_proc,s(index(pendack,host(sK7))))
& elec_2 = index(status,host(sK7))
& index(pendack,host(sK7)) = host(sK5)
& s(index(pendack,host(sK7))) = host(sK6)
& host(sK1) != host(sK7)
& host(sK1) = host(sK4)
& ~ setIn(host(sK3),setEmpty)
& leq(nbr_proc,host(sK1))
& ! [X8] :
( setIn(X8,index(down,host(sK1)))
| host(sK2) = X8
| leq(host(sK1),X8)
| ~ leq(s(zero),X8) )
& elec_1 = index(status,host(sK1))
& ( host(sK2) != index(ldr,host(sK1))
| norm != index(status,host(sK1)) )
& ( wait != index(status,host(sK1))
| host(sK2) != host(index(elid,host(sK1))) )
& ~ leq(host(sK1),host(sK2))
& setIn(sK1,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] :
( ~ leq(host(X13),host(X14))
| ~ elem(m_Halt(X14),queue(host(X13))) )
& ! [X15,X16,X17] :
( ~ leq(host(X15),host(X17))
| ~ elem(m_Ack(X17,X15),queue(host(X16))) )
& ! [X18,X19] :
( ~ setIn(X18,alive)
| ~ setIn(X19,alive)
| X18 = X19
| host(X18) != host(X19) )
& ! [X20,X21] :
( leq(host(X20),index(pendack,host(X21)))
| ~ setIn(X21,alive)
| ~ elem(m_Ack(X21,X20),queue(host(X21))) )
& ! [X22,X23] :
( ~ elem(m_Ack(X23,X22),queue(host(X23)))
| ~ setIn(X23,alive)
| elec_1 != index(status,host(X23)) )
& ! [X24] :
( index(elid,host(X24)) = X24
| ( elec_1 != index(status,host(X24))
& elec_2 != index(status,host(X24)) )
| ~ setIn(X24,alive) )
& ! [X25,X26,X27] :
( ~ setIn(X25,alive)
| host(X25) != index(ldr,host(X25))
| norm != index(status,host(X25))
| ~ setIn(X27,alive)
| ~ elem(m_Down(X26),queue(host(X27)))
| host(X26) != host(X25) )
& ! [X28,X29] :
( leq(index(pendack,host(X29)),host(X28))
| leq(host(X28),host(X29))
| ~ setIn(X28,alive)
| ~ setIn(X29,alive)
| elec_2 != index(status,host(X28))
| elec_2 != index(status,host(X29)) )
& ! [X30,X31,X32] :
( ~ elem(m_Ack(X30,X31),queue(host(X30)))
| ~ setIn(X30,alive)
| ~ setIn(X32,alive)
| host(X32) != host(X31)
| elec_2 != index(status,host(X30))
| elec_2 != index(status,host(X32)) )
& ! [X33,X34] :
( ~ leq(index(pendack,host(X33)),index(pendack,host(X34)))
| leq(host(X33),host(X34))
| ~ setIn(X33,alive)
| ~ setIn(X34,alive)
| elec_2 != index(status,host(X33))
| elec_2 != index(status,host(X34)) )
& ! [X35,X36,X37] :
( ~ setIn(X35,alive)
| host(X35) != index(ldr,host(X35))
| norm != index(status,host(X35))
| leq(index(pendack,host(X37)),host(X35))
| ~ setIn(X37,alive)
| ~ elem(m_Halt(X37),queue(host(X36)))
| elec_2 != index(status,host(X37)) )
& ! [X38,X39,X40,X41] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| ( ~ setIn(sK8(X40,X41),index(down,host(X41)))
& host(X40) != sK8(X40,X41)
& ~ leq(host(X41),sK8(X40,X41))
& leq(s(zero),sK8(X40,X41)) )
| ~ elem(m_Down(X40),queue(host(X41)))
| nbr_proc != host(X41)
| host(X41) != host(X39)
| elec_1 != index(status,host(X41)) )
& ! [X43,X44,X45,X46] :
( ~ setIn(X43,alive)
| host(X43) != index(ldr,host(X43))
| norm != index(status,host(X43))
| ~ setIn(X46,alive)
| ~ elem(m_Down(X45),queue(host(X46)))
| ~ elem(m_Ack(X46,X44),queue(host(X46)))
| ~ leq(nbr_proc,s(index(pendack,host(X46))))
| elec_2 != index(status,host(X46))
| host(X44) != index(pendack,host(X46))
| host(X45) != s(index(pendack,host(X46))) )
& queue(host(sK1)) = cons(m_Down(sK2),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(X42,sK8(X40,X41))],[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(f84,plain,
! [X0,X1] :
( ( ( leq(X0,X1)
& leq(X1,X0) )
| X0 != X1 )
& ( X0 = X1
| ~ leq(X0,X1)
| ~ leq(X1,X0) ) ),
inference(nnf_transformation,[],[f62]) ).
fof(f85,plain,
! [X0,X1] :
( ( ( leq(X0,X1)
& leq(X1,X0) )
| X0 != X1 )
& ( X0 = X1
| ~ leq(X0,X1)
| ~ leq(X1,X0) ) ),
inference(flattening,[],[f84]) ).
fof(f92,plain,
queue(host(sK1)) = cons(m_Down(sK2),sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f94,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| leq(s(zero),sK8(X40,X41))
| ~ elem(m_Down(X40),queue(host(X41)))
| nbr_proc != host(X41)
| host(X41) != host(X39)
| elec_1 != index(status,host(X41)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f95,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| ~ leq(host(X41),sK8(X40,X41))
| ~ elem(m_Down(X40),queue(host(X41)))
| nbr_proc != host(X41)
| host(X41) != host(X39)
| elec_1 != index(status,host(X41)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f96,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| host(X40) != sK8(X40,X41)
| ~ elem(m_Down(X40),queue(host(X41)))
| nbr_proc != host(X41)
| host(X41) != host(X39)
| elec_1 != index(status,host(X41)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f97,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(sK8(X40,X41),index(down,host(X41)))
| ~ elem(m_Down(X40),queue(host(X41)))
| nbr_proc != host(X41)
| host(X41) != host(X39)
| elec_1 != index(status,host(X41)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f116,plain,
elec_1 = index(status,host(sK1)),
inference(cnf_transformation,[],[f79]) ).
fof(f117,plain,
! [X8] :
( setIn(X8,index(down,host(sK1)))
| host(sK2) = X8
| leq(host(sK1),X8)
| ~ leq(s(zero),X8) ),
inference(cnf_transformation,[],[f79]) ).
fof(f118,plain,
leq(nbr_proc,host(sK1)),
inference(cnf_transformation,[],[f79]) ).
fof(f122,plain,
s(index(pendack,host(sK7))) = host(sK6),
inference(cnf_transformation,[],[f79]) ).
fof(f125,plain,
leq(nbr_proc,s(index(pendack,host(sK7)))),
inference(cnf_transformation,[],[f79]) ).
fof(f127,plain,
elem(m_Down(sK6),queue(host(sK7))),
inference(cnf_transformation,[],[f79]) ).
fof(f128,plain,
setIn(sK7,alive),
inference(cnf_transformation,[],[f79]) ).
fof(f140,plain,
! [X2,X0,X1] :
( elem(X0,cons(X1,X2))
| X0 != X1 ),
inference(cnf_transformation,[],[f83]) ).
fof(f144,plain,
! [X0,X1] :
( ~ leq(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f85]) ).
fof(f158,plain,
! [X0] : leq(host(X0),nbr_proc),
inference(cnf_transformation,[],[f5]) ).
fof(f205,definition,
~ sP26(nbr_proc),
introduced(definition,[new_symbols(definition,[sP26])],[inequality_splitting_name_introduction]) ).
fof(f206,definition,
~ sP27(elec_1),
introduced(definition,[new_symbols(definition,[sP27])],[inequality_splitting_name_introduction]) ).
fof(f207,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(sK8(X40,X41),index(down,host(X41)))
| ~ elem(m_Down(X40),queue(host(X41)))
| sP26(host(X41))
| host(X41) != host(X39)
| sP27(index(status,host(X41))) ),
inference(inequality_splitting,[],[f97,f206,f205]) ).
fof(f208,definition,
~ sP28(nbr_proc),
introduced(definition,[new_symbols(definition,[sP28])],[inequality_splitting_name_introduction]) ).
fof(f209,definition,
~ sP29(elec_1),
introduced(definition,[new_symbols(definition,[sP29])],[inequality_splitting_name_introduction]) ).
fof(f210,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| host(X40) != sK8(X40,X41)
| ~ elem(m_Down(X40),queue(host(X41)))
| sP28(host(X41))
| host(X41) != host(X39)
| sP29(index(status,host(X41))) ),
inference(inequality_splitting,[],[f96,f209,f208]) ).
fof(f211,definition,
~ sP30(nbr_proc),
introduced(definition,[new_symbols(definition,[sP30])],[inequality_splitting_name_introduction]) ).
fof(f212,definition,
~ sP31(elec_1),
introduced(definition,[new_symbols(definition,[sP31])],[inequality_splitting_name_introduction]) ).
fof(f213,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| ~ leq(host(X41),sK8(X40,X41))
| ~ elem(m_Down(X40),queue(host(X41)))
| sP30(host(X41))
| host(X41) != host(X39)
| sP31(index(status,host(X41))) ),
inference(inequality_splitting,[],[f95,f212,f211]) ).
fof(f214,definition,
~ sP32(nbr_proc),
introduced(definition,[new_symbols(definition,[sP32])],[inequality_splitting_name_introduction]) ).
fof(f215,definition,
~ sP33(elec_1),
introduced(definition,[new_symbols(definition,[sP33])],[inequality_splitting_name_introduction]) ).
fof(f216,plain,
! [X40,X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| leq(s(zero),sK8(X40,X41))
| ~ elem(m_Down(X40),queue(host(X41)))
| sP32(host(X41))
| host(X41) != host(X39)
| sP33(index(status,host(X41))) ),
inference(inequality_splitting,[],[f94,f215,f214]) ).
fof(f233,plain,
! [X2,X1] : elem(X1,cons(X1,X2)),
inference(equality_resolution,[],[f140]) ).
fof(f247,plain,
! [X40,X41] :
( ~ setIn(sK8(X40,X41),index(down,host(X41)))
| ~ elem(m_Down(X40),queue(host(X41)))
| sP45(X41) ),
inference(cnf_transformation,[],[f247_D]) ).
fof(f247_D,definition,
! [X41] :
( ! [X40] :
( ~ setIn(sK8(X40,X41),index(down,host(X41)))
| ~ elem(m_Down(X40),queue(host(X41))) )
<=> ~ sP45(X41) ),
introduced(definition,[new_symbols(definition,[sP45])],[general_splitting_component_introduction]) ).
fof(f248,plain,
! [X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| sP26(host(X41))
| host(X41) != host(X39)
| sP27(index(status,host(X41)))
| ~ sP45(X41) ),
inference(general_splitting,[],[f207,f247_D]) ).
fof(f249,plain,
! [X38,X39] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive)
| sP46(X39) ),
inference(cnf_transformation,[],[f249_D]) ).
fof(f249_D,definition,
! [X39] :
( ! [X38] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive) )
<=> ~ sP46(X39) ),
introduced(definition,[new_symbols(definition,[sP46])],[general_splitting_component_introduction]) ).
fof(f250,plain,
! [X41,X39] :
( host(X41) != host(X39)
| sP26(host(X41))
| sP27(index(status,host(X41)))
| ~ sP45(X41)
| ~ sP46(X39) ),
inference(general_splitting,[],[f248,f249_D]) ).
fof(f251,plain,
! [X40,X41] :
( host(X40) != sK8(X40,X41)
| ~ elem(m_Down(X40),queue(host(X41)))
| sP47(X41) ),
inference(cnf_transformation,[],[f251_D]) ).
fof(f251_D,definition,
! [X41] :
( ! [X40] :
( host(X40) != sK8(X40,X41)
| ~ elem(m_Down(X40),queue(host(X41))) )
<=> ~ sP47(X41) ),
introduced(definition,[new_symbols(definition,[sP47])],[general_splitting_component_introduction]) ).
fof(f252,plain,
! [X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| sP28(host(X41))
| host(X41) != host(X39)
| sP29(index(status,host(X41)))
| ~ sP47(X41) ),
inference(general_splitting,[],[f210,f251_D]) ).
fof(f253,plain,
! [X38,X39] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive)
| sP48(X39) ),
inference(cnf_transformation,[],[f253_D]) ).
fof(f253_D,definition,
! [X39] :
( ! [X38] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive) )
<=> ~ sP48(X39) ),
introduced(definition,[new_symbols(definition,[sP48])],[general_splitting_component_introduction]) ).
fof(f254,plain,
! [X41,X39] :
( host(X41) != host(X39)
| sP28(host(X41))
| sP29(index(status,host(X41)))
| ~ sP47(X41)
| ~ sP48(X39) ),
inference(general_splitting,[],[f252,f253_D]) ).
fof(f255,plain,
! [X40,X41] :
( ~ leq(host(X41),sK8(X40,X41))
| ~ elem(m_Down(X40),queue(host(X41)))
| sP49(X41) ),
inference(cnf_transformation,[],[f255_D]) ).
fof(f255_D,definition,
! [X41] :
( ! [X40] :
( ~ leq(host(X41),sK8(X40,X41))
| ~ elem(m_Down(X40),queue(host(X41))) )
<=> ~ sP49(X41) ),
introduced(definition,[new_symbols(definition,[sP49])],[general_splitting_component_introduction]) ).
fof(f256,plain,
! [X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| sP30(host(X41))
| host(X41) != host(X39)
| sP31(index(status,host(X41)))
| ~ sP49(X41) ),
inference(general_splitting,[],[f213,f255_D]) ).
fof(f257,plain,
! [X38,X39] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive)
| sP50(X39) ),
inference(cnf_transformation,[],[f257_D]) ).
fof(f257_D,definition,
! [X39] :
( ! [X38] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive) )
<=> ~ sP50(X39) ),
introduced(definition,[new_symbols(definition,[sP50])],[general_splitting_component_introduction]) ).
fof(f258,plain,
! [X41,X39] :
( host(X41) != host(X39)
| sP30(host(X41))
| sP31(index(status,host(X41)))
| ~ sP49(X41)
| ~ sP50(X39) ),
inference(general_splitting,[],[f256,f257_D]) ).
fof(f259,plain,
! [X40,X41] :
( ~ elem(m_Down(X40),queue(host(X41)))
| leq(s(zero),sK8(X40,X41))
| sP51(X41) ),
inference(cnf_transformation,[],[f259_D]) ).
fof(f259_D,definition,
! [X41] :
( ! [X40] :
( ~ elem(m_Down(X40),queue(host(X41)))
| leq(s(zero),sK8(X40,X41)) )
<=> ~ sP51(X41) ),
introduced(definition,[new_symbols(definition,[sP51])],[general_splitting_component_introduction]) ).
fof(f260,plain,
! [X38,X41,X39] :
( ~ setIn(X38,alive)
| ~ elem(m_Down(X39),queue(host(X38)))
| sP32(host(X41))
| host(X41) != host(X39)
| sP33(index(status,host(X41)))
| ~ sP51(X41) ),
inference(general_splitting,[],[f216,f259_D]) ).
fof(f261,plain,
! [X38,X39] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive)
| sP52(X39) ),
inference(cnf_transformation,[],[f261_D]) ).
fof(f261_D,definition,
! [X39] :
( ! [X38] :
( ~ elem(m_Down(X39),queue(host(X38)))
| ~ setIn(X38,alive) )
<=> ~ sP52(X39) ),
introduced(definition,[new_symbols(definition,[sP52])],[general_splitting_component_introduction]) ).
fof(f262,plain,
! [X41,X39] :
( host(X41) != host(X39)
| sP32(host(X41))
| sP33(index(status,host(X41)))
| ~ sP51(X41)
| ~ sP52(X39) ),
inference(general_splitting,[],[f260,f261_D]) ).
fof(f297,plain,
( ~ leq(host(sK1),nbr_proc)
| nbr_proc = host(sK1) ),
inference(resolution,[],[f118,f144]) ).
fof(f299,plain,
nbr_proc = host(sK1),
inference(forward_subsumption_resolution,[],[f297,f158]) ).
fof(f303,plain,
! [X0] : leq(host(X0),host(sK1)),
inference(superposition,[],[f158,f299]) ).
fof(f304,plain,
~ sP26(host(sK1)),
inference(superposition,[],[f205,f299]) ).
fof(f305,plain,
~ sP28(host(sK1)),
inference(superposition,[],[f208,f299]) ).
fof(f306,plain,
~ sP30(host(sK1)),
inference(superposition,[],[f211,f299]) ).
fof(f307,plain,
~ sP32(host(sK1)),
inference(superposition,[],[f214,f299]) ).
fof(f314,plain,
~ sP27(index(status,host(sK1))),
inference(superposition,[],[f206,f116]) ).
fof(f315,plain,
~ sP29(index(status,host(sK1))),
inference(superposition,[],[f209,f116]) ).
fof(f316,plain,
~ sP31(index(status,host(sK1))),
inference(superposition,[],[f212,f116]) ).
fof(f317,plain,
~ sP33(index(status,host(sK1))),
inference(superposition,[],[f215,f116]) ).
fof(f329,plain,
( ~ leq(s(index(pendack,host(sK7))),nbr_proc)
| nbr_proc = s(index(pendack,host(sK7))) ),
inference(resolution,[],[f125,f144]) ).
fof(f333,plain,
( ~ leq(s(index(pendack,host(sK7))),host(sK1))
| nbr_proc = s(index(pendack,host(sK7))) ),
inference(forward_demodulation,[],[f329,f299]) ).
fof(f335,plain,
( host(sK1) = s(index(pendack,host(sK7)))
| ~ leq(s(index(pendack,host(sK7))),host(sK1)) ),
inference(forward_demodulation,[],[f333,f299]) ).
fof(f338,definition,
( spl55_8
<=> leq(s(index(pendack,host(sK7))),host(sK1)) ),
introduced(definition,[new_symbols(definition,[spl55_8])],[avatar_definition]) ).
fof(f340,plain,
( ~ leq(s(index(pendack,host(sK7))),host(sK1))
| spl55_8 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f342,definition,
( spl55_9
<=> host(sK1) = s(index(pendack,host(sK7))) ),
introduced(definition,[new_symbols(definition,[spl55_9])],[avatar_definition]) ).
fof(f344,plain,
( host(sK1) = s(index(pendack,host(sK7)))
| ~ spl55_9 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
( ~ spl55_8
| spl55_9 ),
inference(avatar_split_clause,[],[f335,f342,f338]) ).
fof(f353,plain,
elem(m_Down(sK2),queue(host(sK1))),
inference(superposition,[],[f233,f92]) ).
fof(f393,plain,
leq(s(index(pendack,host(sK7))),host(sK1)),
inference(superposition,[],[f303,f122]) ).
fof(f419,plain,
( ~ setIn(sK7,alive)
| sP46(sK6) ),
inference(resolution,[],[f249,f127]) ).
fof(f425,plain,
sP46(sK6),
inference(forward_subsumption_resolution,[],[f419,f128]) ).
fof(f431,plain,
( ~ setIn(sK7,alive)
| sP48(sK6) ),
inference(resolution,[],[f253,f127]) ).
fof(f437,plain,
sP48(sK6),
inference(forward_subsumption_resolution,[],[f431,f128]) ).
fof(f443,plain,
( ~ setIn(sK7,alive)
| sP50(sK6) ),
inference(resolution,[],[f257,f127]) ).
fof(f449,plain,
sP50(sK6),
inference(forward_subsumption_resolution,[],[f443,f128]) ).
fof(f455,plain,
( ~ setIn(sK7,alive)
| sP52(sK6) ),
inference(resolution,[],[f261,f127]) ).
fof(f461,plain,
sP52(sK6),
inference(forward_subsumption_resolution,[],[f455,f128]) ).
fof(f517,plain,
! [X0] :
( ~ leq(s(index(pendack,host(sK7))),sK8(X0,sK6))
| ~ elem(m_Down(X0),queue(s(index(pendack,host(sK7)))))
| sP49(sK6) ),
inference(superposition,[],[f255,f122]) ).
fof(f518,plain,
( ! [X0] :
( ~ leq(host(sK1),sK8(X0,sK6))
| ~ elem(m_Down(X0),queue(s(index(pendack,host(sK7)))))
| sP49(sK6) )
| ~ spl55_9 ),
inference(forward_demodulation,[],[f517,f344]) ).
fof(f528,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| ~ leq(host(sK1),sK8(X0,sK6))
| sP49(sK6) )
| ~ spl55_9 ),
inference(forward_demodulation,[],[f518,f344]) ).
fof(f531,definition,
( spl55_22
<=> sP49(sK6) ),
introduced(definition,[new_symbols(definition,[spl55_22])],[avatar_definition]) ).
fof(f533,plain,
( sP49(sK6)
| ~ spl55_22 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f535,definition,
( spl55_23
<=> ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| ~ leq(host(sK1),sK8(X0,sK6)) ) ),
introduced(definition,[new_symbols(definition,[spl55_23])],[avatar_definition]) ).
fof(f536,plain,
( ! [X0] :
( ~ leq(host(sK1),sK8(X0,sK6))
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl55_23 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f537,plain,
( spl55_22
| spl55_23
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f528,f342,f535,f531]) ).
fof(f548,plain,
( $false
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f393,f340]) ).
fof(f549,plain,
spl55_8,
inference(avatar_contradiction_clause,[],[f548]) ).
fof(f558,plain,
! [X0] :
( ~ elem(m_Down(X0),queue(s(index(pendack,host(sK7)))))
| leq(s(zero),sK8(X0,sK6))
| sP51(sK6) ),
inference(superposition,[],[f259,f122]) ).
fof(f559,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| leq(s(zero),sK8(X0,sK6))
| sP51(sK6) )
| ~ spl55_9 ),
inference(forward_demodulation,[],[f558,f344]) ).
fof(f588,definition,
( spl55_33
<=> sP51(sK6) ),
introduced(definition,[new_symbols(definition,[spl55_33])],[avatar_definition]) ).
fof(f590,plain,
( sP51(sK6)
| ~ spl55_33 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f592,definition,
( spl55_34
<=> ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| leq(s(zero),sK8(X0,sK6)) ) ),
introduced(definition,[new_symbols(definition,[spl55_34])],[avatar_definition]) ).
fof(f593,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| leq(s(zero),sK8(X0,sK6)) )
| ~ spl55_34 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f594,plain,
( spl55_33
| spl55_34
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f559,f342,f592,f588]) ).
fof(f667,plain,
! [X0] :
( ~ setIn(sK8(X0,sK6),index(down,s(index(pendack,host(sK7)))))
| ~ elem(m_Down(X0),queue(s(index(pendack,host(sK7)))))
| sP45(sK6) ),
inference(superposition,[],[f247,f122]) ).
fof(f668,plain,
( ! [X0] :
( ~ setIn(sK8(X0,sK6),index(down,host(sK1)))
| ~ elem(m_Down(X0),queue(s(index(pendack,host(sK7)))))
| sP45(sK6) )
| ~ spl55_9 ),
inference(forward_demodulation,[],[f667,f344]) ).
fof(f678,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| ~ setIn(sK8(X0,sK6),index(down,host(sK1)))
| sP45(sK6) )
| ~ spl55_9 ),
inference(forward_demodulation,[],[f668,f344]) ).
fof(f681,definition,
( spl55_48
<=> sP45(sK6) ),
introduced(definition,[new_symbols(definition,[spl55_48])],[avatar_definition]) ).
fof(f683,plain,
( sP45(sK6)
| ~ spl55_48 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f685,definition,
( spl55_49
<=> ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| ~ setIn(sK8(X0,sK6),index(down,host(sK1))) ) ),
introduced(definition,[new_symbols(definition,[spl55_49])],[avatar_definition]) ).
fof(f686,plain,
( ! [X0] :
( ~ setIn(sK8(X0,sK6),index(down,host(sK1)))
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl55_49 ),
inference(avatar_component_clause,[],[f685]) ).
fof(f687,plain,
( spl55_48
| spl55_49
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f678,f342,f685,f681]) ).
fof(f744,plain,
! [X0] :
( host(X0) != s(index(pendack,host(sK7)))
| sP26(s(index(pendack,host(sK7))))
| sP27(index(status,s(index(pendack,host(sK7)))))
| ~ sP45(sK6)
| ~ sP46(X0) ),
inference(superposition,[],[f250,f122]) ).
fof(f759,plain,
( ! [X0] :
( host(X0) != s(index(pendack,host(sK7)))
| sP26(s(index(pendack,host(sK7))))
| sP27(index(status,s(index(pendack,host(sK7)))))
| ~ sP46(X0) )
| ~ spl55_48 ),
inference(forward_subsumption_resolution,[],[f744,f683]) ).
fof(f771,plain,
( ! [X0] :
( host(X0) != host(sK1)
| sP26(s(index(pendack,host(sK7))))
| sP27(index(status,s(index(pendack,host(sK7)))))
| ~ sP46(X0) )
| ~ spl55_9
| ~ spl55_48 ),
inference(forward_demodulation,[],[f759,f344]) ).
fof(f786,plain,
( ! [X0] :
( sP26(host(sK1))
| host(X0) != host(sK1)
| sP27(index(status,s(index(pendack,host(sK7)))))
| ~ sP46(X0) )
| ~ spl55_9
| ~ spl55_48 ),
inference(forward_demodulation,[],[f771,f344]) ).
fof(f788,plain,
( ! [X0] :
( host(X0) != host(sK1)
| sP27(index(status,s(index(pendack,host(sK7)))))
| ~ sP46(X0) )
| ~ spl55_9
| ~ spl55_48 ),
inference(forward_subsumption_resolution,[],[f786,f304]) ).
fof(f790,definition,
( spl55_63
<=> ! [X0] :
( host(X0) != host(sK1)
| ~ sP46(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_63])],[avatar_definition]) ).
fof(f791,plain,
( ! [X0] :
( host(X0) != host(sK1)
| ~ sP46(X0) )
| ~ spl55_63 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f793,plain,
( ! [X0] :
( sP27(index(status,host(sK1)))
| host(X0) != host(sK1)
| ~ sP46(X0) )
| ~ spl55_9
| ~ spl55_48 ),
inference(forward_demodulation,[],[f788,f344]) ).
fof(f794,plain,
( ! [X0] :
( host(X0) != host(sK1)
| ~ sP46(X0) )
| ~ spl55_9
| ~ spl55_48 ),
inference(forward_subsumption_resolution,[],[f793,f314]) ).
fof(f795,plain,
( spl55_63
| ~ spl55_9
| ~ spl55_48 ),
inference(avatar_split_clause,[],[f794,f681,f342,f790]) ).
fof(f802,plain,
! [X0] :
( sP29(index(status,host(X0)))
| sP28(host(X0))
| ~ sP47(X0)
| ~ sP48(X0) ),
inference(equality_resolution,[],[f254]) ).
fof(f856,definition,
( spl55_74
<=> sP47(sK6) ),
introduced(definition,[new_symbols(definition,[spl55_74])],[avatar_definition]) ).
fof(f857,plain,
( sP47(sK6)
| ~ spl55_74 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f858,plain,
( ~ sP47(sK6)
| spl55_74 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f866,plain,
! [X0] :
( sP31(index(status,host(X0)))
| sP30(host(X0))
| ~ sP49(X0)
| ~ sP50(X0) ),
inference(equality_resolution,[],[f258]) ).
fof(f922,plain,
! [X0] :
( sP33(index(status,host(X0)))
| sP32(host(X0))
| ~ sP51(X0)
| ~ sP52(X0) ),
inference(equality_resolution,[],[f262]) ).
fof(f1124,plain,
( host(sK1) != s(index(pendack,host(sK7)))
| ~ sP46(sK6)
| ~ spl55_63 ),
inference(superposition,[],[f791,f122]) ).
fof(f1127,plain,
( ~ sP46(sK6)
| ~ spl55_9
| ~ spl55_63 ),
inference(forward_subsumption_resolution,[],[f1124,f344]) ).
fof(f1129,plain,
( $false
| ~ spl55_9
| ~ spl55_63 ),
inference(forward_subsumption_resolution,[],[f1127,f425]) ).
fof(f1130,plain,
( ~ spl55_9
| ~ spl55_63 ),
inference(avatar_contradiction_clause,[],[f1129]) ).
fof(f1333,plain,
( sP29(index(status,s(index(pendack,host(sK7)))))
| sP28(s(index(pendack,host(sK7))))
| ~ sP47(sK6)
| ~ sP48(sK6) ),
inference(superposition,[],[f802,f122]) ).
fof(f1358,plain,
( sP31(index(status,s(index(pendack,host(sK7)))))
| sP30(s(index(pendack,host(sK7))))
| ~ sP49(sK6)
| ~ sP50(sK6) ),
inference(superposition,[],[f866,f122]) ).
fof(f1383,plain,
( sP33(index(status,s(index(pendack,host(sK7)))))
| sP32(s(index(pendack,host(sK7))))
| ~ sP51(sK6)
| ~ sP52(sK6) ),
inference(superposition,[],[f922,f122]) ).
fof(f1458,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK8(X0,sK6)
| leq(host(sK1),sK8(X0,sK6))
| ~ leq(s(zero),sK8(X0,sK6)) )
| ~ spl55_49 ),
inference(resolution,[],[f686,f117]) ).
fof(f1459,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK8(X0,sK6)
| ~ leq(s(zero),sK8(X0,sK6)) )
| ~ spl55_23
| ~ spl55_49 ),
inference(forward_subsumption_resolution,[],[f1458,f536]) ).
fof(f1460,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK8(X0,sK6) )
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49 ),
inference(forward_subsumption_resolution,[],[f1459,f593]) ).
fof(f2129,plain,
( host(sK2) = sK8(sK2,sK6)
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49 ),
inference(resolution,[],[f1460,f353]) ).
fof(f2145,plain,
( host(sK2) != host(sK2)
| ~ elem(m_Down(sK2),queue(host(sK6)))
| sP47(sK6)
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49 ),
inference(superposition,[],[f251,f2129]) ).
fof(f2146,plain,
( ~ elem(m_Down(sK2),queue(host(sK6)))
| sP47(sK6)
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49 ),
inference(trivial_inequality_removal,[],[f2145]) ).
fof(f2147,plain,
( ~ elem(m_Down(sK2),queue(host(sK6)))
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49
| spl55_74 ),
inference(forward_subsumption_resolution,[],[f2146,f858]) ).
fof(f2151,plain,
( ~ elem(m_Down(sK2),queue(s(index(pendack,host(sK7)))))
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49
| spl55_74 ),
inference(forward_demodulation,[],[f2147,f122]) ).
fof(f2154,plain,
( ~ elem(m_Down(sK2),queue(host(sK1)))
| ~ spl55_9
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49
| spl55_74 ),
inference(forward_demodulation,[],[f2151,f344]) ).
fof(f2157,plain,
( $false
| ~ spl55_9
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49
| spl55_74 ),
inference(forward_subsumption_resolution,[],[f2154,f353]) ).
fof(f2158,plain,
( ~ spl55_9
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49
| spl55_74 ),
inference(avatar_contradiction_clause,[],[f2157]) ).
fof(f2159,plain,
( sP29(index(status,s(index(pendack,host(sK7)))))
| sP28(s(index(pendack,host(sK7))))
| ~ sP48(sK6)
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f1333,f857]) ).
fof(f2161,plain,
( sP29(index(status,s(index(pendack,host(sK7)))))
| sP28(s(index(pendack,host(sK7))))
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f2159,f437]) ).
fof(f2163,plain,
( sP29(index(status,host(sK1)))
| sP28(s(index(pendack,host(sK7))))
| ~ spl55_9
| ~ spl55_74 ),
inference(forward_demodulation,[],[f2161,f344]) ).
fof(f2165,plain,
( sP28(s(index(pendack,host(sK7))))
| ~ spl55_9
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f2163,f315]) ).
fof(f2167,plain,
( sP28(host(sK1))
| ~ spl55_9
| ~ spl55_74 ),
inference(forward_demodulation,[],[f2165,f344]) ).
fof(f2169,plain,
( $false
| ~ spl55_9
| ~ spl55_74 ),
inference(forward_subsumption_resolution,[],[f2167,f305]) ).
fof(f2170,plain,
( ~ spl55_9
| ~ spl55_74 ),
inference(avatar_contradiction_clause,[],[f2169]) ).
fof(f2176,plain,
( sP31(index(status,s(index(pendack,host(sK7)))))
| sP30(s(index(pendack,host(sK7))))
| ~ sP50(sK6)
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f1358,f533]) ).
fof(f2179,plain,
( sP31(index(status,s(index(pendack,host(sK7)))))
| sP30(s(index(pendack,host(sK7))))
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f2176,f449]) ).
fof(f2181,plain,
( sP31(index(status,host(sK1)))
| sP30(s(index(pendack,host(sK7))))
| ~ spl55_9
| ~ spl55_22 ),
inference(forward_demodulation,[],[f2179,f344]) ).
fof(f2183,plain,
( sP30(s(index(pendack,host(sK7))))
| ~ spl55_9
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f2181,f316]) ).
fof(f2185,plain,
( sP30(host(sK1))
| ~ spl55_9
| ~ spl55_22 ),
inference(forward_demodulation,[],[f2183,f344]) ).
fof(f2187,plain,
( $false
| ~ spl55_9
| ~ spl55_22 ),
inference(forward_subsumption_resolution,[],[f2185,f306]) ).
fof(f2188,plain,
( ~ spl55_9
| ~ spl55_22 ),
inference(avatar_contradiction_clause,[],[f2187]) ).
fof(f2193,plain,
( sP33(index(status,s(index(pendack,host(sK7)))))
| sP32(s(index(pendack,host(sK7))))
| ~ sP52(sK6)
| ~ spl55_33 ),
inference(forward_subsumption_resolution,[],[f1383,f590]) ).
fof(f2198,plain,
( sP33(index(status,s(index(pendack,host(sK7)))))
| sP32(s(index(pendack,host(sK7))))
| ~ spl55_33 ),
inference(forward_subsumption_resolution,[],[f2193,f461]) ).
fof(f2202,plain,
( sP33(index(status,host(sK1)))
| sP32(s(index(pendack,host(sK7))))
| ~ spl55_9
| ~ spl55_33 ),
inference(forward_demodulation,[],[f2198,f344]) ).
fof(f2206,plain,
( sP32(s(index(pendack,host(sK7))))
| ~ spl55_9
| ~ spl55_33 ),
inference(forward_subsumption_resolution,[],[f2202,f317]) ).
fof(f2208,plain,
( sP32(host(sK1))
| ~ spl55_9
| ~ spl55_33 ),
inference(forward_demodulation,[],[f2206,f344]) ).
fof(f2210,plain,
( $false
| ~ spl55_9
| ~ spl55_33 ),
inference(forward_subsumption_resolution,[],[f2208,f307]) ).
fof(f2211,plain,
( ~ spl55_9
| ~ spl55_33 ),
inference(avatar_contradiction_clause,[],[f2210]) ).
cnf(s5,plain,
( ~ spl55_8
| spl55_9 ),
inference(sat_conversion,[],[f345]) ).
cnf(s21,plain,
( ~ spl55_9
| spl55_22
| spl55_23 ),
inference(sat_conversion,[],[f537]) ).
cnf(s24,plain,
spl55_8,
inference(sat_conversion,[],[f549]) ).
cnf(s29,plain,
( ~ spl55_9
| spl55_33
| spl55_34 ),
inference(sat_conversion,[],[f594]) ).
cnf(s37,plain,
( ~ spl55_9
| spl55_48
| spl55_49 ),
inference(sat_conversion,[],[f687]) ).
cnf(s47,plain,
( ~ spl55_9
| ~ spl55_48
| spl55_63 ),
inference(sat_conversion,[],[f795]) ).
cnf(s79,plain,
( ~ spl55_9
| ~ spl55_63 ),
inference(sat_conversion,[],[f1130]) ).
cnf(s98,plain,
( ~ spl55_9
| ~ spl55_23
| ~ spl55_34
| ~ spl55_49
| spl55_74 ),
inference(sat_conversion,[],[f2158]) ).
cnf(s99,plain,
( ~ spl55_9
| ~ spl55_74 ),
inference(sat_conversion,[],[f2170]) ).
cnf(s103,plain,
( ~ spl55_9
| ~ spl55_22 ),
inference(sat_conversion,[],[f2188]) ).
cnf(s106,plain,
( ~ spl55_9
| ~ spl55_33 ),
inference(sat_conversion,[],[f2211]) ).
cnf(s109,plain,
spl55_9,
inference(rat,[],[s5,s24]) ).
cnf(s110,plain,
~ spl55_33,
inference(rat,[],[s106,s109]) ).
cnf(s111,plain,
~ spl55_22,
inference(rat,[],[s103,s109]) ).
cnf(s112,plain,
~ spl55_74,
inference(rat,[],[s99,s109]) ).
cnf(s114,plain,
~ spl55_63,
inference(rat,[],[s79,s109]) ).
cnf(s118,plain,
~ spl55_48,
inference(rat,[],[s47,s114,s109]) ).
cnf(s120,plain,
spl55_34,
inference(rat,[],[s29,s109,s110]) ).
cnf(s122,plain,
spl55_23,
inference(rat,[],[s21,s109,s111]) ).
cnf(s124,plain,
spl55_49,
inference(rat,[],[s37,s109,s118]) ).
cnf(s125,plain,
$false,
inference(rat,[],[s98,s112,s124,s109,s120,s122]) ).
fof(f2214,plain,
$false,
inference(avatar_sat_refutation,[],[s125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV467+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.06/0.18 % Computer : n018.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 11:12:25 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.22 Running first-order theorem proving
% 0.06/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
% 3.02/1.12 % (3306051)Detected formulas, will run a generic FOF schedule.
% 3.02/1.12 % (3306150)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3111946411:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.02/1.12 % (3306145)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=3632040470:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.02/1.12 % (3306148)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=359439476:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.02/1.12 % (3306143)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=865643291:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.02/1.12 % (3306146)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=895907984:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.02/1.12 % (3306150)Instruction limit reached!
% 3.02/1.12 % (3306150)------------------------------
% 3.02/1.12 % (3306150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.12 % (3306150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.12 % (3306150)CaDiCaL version: 2.1.3
% 3.02/1.12 % (3306150)Termination reason: Instruction limit
% 3.02/1.12 % (3306150)Termination phase: Saturation
% 3.02/1.12 % (3306150)Time elapsed: 0.041 s
% 3.02/1.12 % (3306150)Peak memory usage: 88 MB
% 3.02/1.12 % (3306150)Instructions burned: 119 (million)
% 3.02/1.12 % (3306152)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1230813651:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.02/1.12 % (3306153)dis-21_1_sil=8000:lcm=predicate:random_seed=440790261: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)
% 3.02/1.12 % (3306148)First to succeed.
% 3.02/1.12 % (3306148)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3306051"
% 3.02/1.12 % (3306153)Instruction limit reached!
% 3.02/1.12 % (3306153)------------------------------
% 3.02/1.12 % (3306153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.12 % (3306153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.12 % (3306153)CaDiCaL version: 2.1.3
% 3.02/1.12 % (3306153)Termination reason: Instruction limit
% 3.02/1.12 % (3306153)Termination phase: Saturation
% 3.02/1.12 % (3306153)Time elapsed: 0.084 s
% 3.02/1.12 % (3306153)Peak memory usage: 90 MB
% 3.02/1.12 % (3306153)Instructions burned: 131 (million)
% 3.02/1.12 % (3306152)Instruction limit reached!
% 3.02/1.12 % (3306152)------------------------------
% 3.02/1.12 % (3306152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.12 % (3306152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.12 % (3306152)CaDiCaL version: 2.1.3
% 3.02/1.12 % (3306152)Termination reason: Instruction limit
% 3.02/1.12 % (3306152)Termination phase: Saturation
% 3.02/1.12 % (3306152)Time elapsed: 0.100 s
% 3.02/1.12 % (3306152)Peak memory usage: 90 MB
% 3.02/1.12 % (3306152)Instructions burned: 139 (million)
% 3.02/1.12 % (3306198)lrs+10_1_sil=8000:sp=occurrence:random_seed=1190976265:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.02/1.12 % (3306198)Instruction limit reached!
% 3.02/1.12 % (3306198)------------------------------
% 3.02/1.12 % (3306198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.12 % (3306198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.12 % (3306198)CaDiCaL version: 2.1.3
% 3.02/1.12 % (3306198)Termination reason: Instruction limit
% 3.02/1.12 % (3306198)Termination phase: Saturation
% 3.02/1.12 % (3306198)Time elapsed: 0.100 s
% 3.02/1.12 % (3306198)Peak memory usage: 91 MB
% 3.02/1.12 % (3306198)Instructions burned: 285 (million)
% 3.02/1.12 % (3306218)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4030843711:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.02/1.12 % (3306219)lrs+1011_1_sil=32000:sp=occurrence:random_seed=826435260:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 3.02/1.12 % (3306148)Refutation found. Thanks to Tanya!
% 3.02/1.12 % SZS status Theorem for theBenchmark
% 3.02/1.12 % SZS output start Proof for theBenchmark
% See solution above
% 3.80/1.22 % (3306148)------------------------------
% 3.80/1.22 % (3306148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.80/1.22 % (3306148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.80/1.22 % (3306148)CaDiCaL version: 2.1.3
% 3.80/1.22 % (3306148)Termination reason: Refutation
% 3.80/1.22 % (3306148)Time elapsed: 0.048 s
% 3.80/1.22 % (3306148)Peak memory usage: 90 MB
% 3.80/1.22 % (3306148)Instructions burned: 71 (million)
% 3.80/1.22 % (3306148)------------------------------
% 3.80/1.22 % (3306148)------------------------------
% 3.80/1.22 % (3306051)Success in time 0.449 s
% 3.80/1.22 % Vampire exiting
%------------------------------------------------------------------------------