%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV448+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 : n013.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:50 PM UTC 2026
% Result : Theorem 5.00s 1.68s
% Output : Refutation 6.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 36
% Syntax : Number of formulae : 253 ( 58 unt; 29 def)
% Number of atoms : 1173 ( 333 equ)
% Maximal formula atoms : 65 ( 4 avg)
% Number of connectives : 1528 ( 608 ~; 603 |; 238 &)
% ( 21 <=>; 58 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 34 ( 32 usr; 16 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 19 con; 0-2 aty)
% Number of variables : 314 ( 2 sgn 293 !; 21 ?)
% 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(f60,axiom,
! [X0] : leq(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_59) ).
fof(f61,axiom,
! [X0,X1] :
( leq(X0,X1)
| leq(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_60) ).
fof(f62,axiom,
! [X0,X1] :
( ( leq(X0,X1)
& leq(X1,X0) )
<=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_61) ).
fof(f63,axiom,
! [X0,X1,X2] :
( ( leq(X0,X1)
& leq(X1,X2) )
=> leq(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_62) ).
fof(f67,conjecture,
! [X0,X1,X2,X3] :
( ( ! [X4,X5] :
( elem(m_Ldr(X5),queue(host(X4)))
=> ~ leq(host(X4),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,X5] :
( ( setIn(X4,alive)
& setIn(X5,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm
& index(status,host(X5)) = norm
& index(ldr,host(X5)) = host(X5) )
=> X5 = X4 )
& ! [X4,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Down(X6),queue(host(X5)))
& leq(nbr_proc,index(pendack,host(X5)))
& index(status,host(X5)) = elec_2
& host(X6) = index(pendack,host(X5)) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [X4,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Ack(X5,X6),queue(host(X5)))
& leq(nbr_proc,index(pendack,host(X5)))
& index(status,host(X5)) = elec_2
& host(X6) = index(pendack,host(X5)) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [X4,X6,X5] :
( ( ! [X7] :
( ( ~ leq(host(X5),X7)
& leq(s(zero),X7) )
=> ( setIn(X7,index(down,host(X5)))
| X7 = host(X6) ) )
& ~ leq(host(X5),host(X4))
& elem(m_Down(X6),queue(host(X5)))
& index(status,host(X5)) = elec_1 )
=> ~ ( 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)
=> ! [X7] :
( host(X2) = host(X7)
=> ! [X8] :
( host(X2) != host(X8)
=> ( ( setIn(X7,alive)
& setIn(X8,alive)
& host(X2) = host(X7)
& index(ldr,host(X8)) = host(X8)
& index(status,host(X8)) = norm )
=> X8 = X7 ) ) ) ) ) ) ) ) ) ),
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] :
( ( 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,X5] :
( ( setIn(X4,alive)
& setIn(X5,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm
& index(status,host(X5)) = norm
& index(ldr,host(X5)) = host(X5) )
=> X5 = X4 )
& ! [X4,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Down(X6),queue(host(X5)))
& leq(nbr_proc,index(pendack,host(X5)))
& index(status,host(X5)) = elec_2
& host(X6) = index(pendack,host(X5)) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [X4,X6,X5] :
( ( setIn(X5,alive)
& elem(m_Ack(X5,X6),queue(host(X5)))
& leq(nbr_proc,index(pendack,host(X5)))
& index(status,host(X5)) = elec_2
& host(X6) = index(pendack,host(X5)) )
=> ~ ( setIn(X4,alive)
& index(ldr,host(X4)) = host(X4)
& index(status,host(X4)) = norm ) )
& ! [X4,X6,X5] :
( ( ! [X7] :
( ( ~ leq(host(X5),X7)
& leq(s(zero),X7) )
=> ( setIn(X7,index(down,host(X5)))
| X7 = host(X6) ) )
& ~ leq(host(X5),host(X4))
& elem(m_Down(X6),queue(host(X5)))
& index(status,host(X5)) = elec_1 )
=> ~ ( 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)
=> ! [X7] :
( host(X2) = host(X7)
=> ! [X8] :
( host(X2) != host(X8)
=> ( ( setIn(X7,alive)
& setIn(X8,alive)
& host(X2) = host(X7)
& index(ldr,host(X8)) = host(X8)
& index(status,host(X8)) = norm )
=> X8 = X7 ) ) ) ) ) ) ) ) ) ),
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] :
( ( X6 != X7
& host(X6) = host(X7) )
=> ( ~ setIn(X6,alive)
| ~ setIn(X7,alive) ) )
& ! [X8] :
( ( ( elec_1 = index(status,host(X8))
| elec_2 = index(status,host(X8)) )
& setIn(X8,alive) )
=> index(elid,host(X8)) = X8 )
& ! [X9,X10] :
( ( setIn(X9,alive)
& setIn(X10,alive)
& host(X9) = index(ldr,host(X9))
& norm = index(status,host(X9))
& norm = index(status,host(X10))
& host(X10) = index(ldr,host(X10)) )
=> X9 = X10 )
& ! [X11,X12,X13] :
( ( setIn(X13,alive)
& elem(m_Down(X12),queue(host(X13)))
& leq(nbr_proc,index(pendack,host(X13)))
& elec_2 = index(status,host(X13))
& index(pendack,host(X13)) = host(X12) )
=> ~ ( setIn(X11,alive)
& host(X11) = index(ldr,host(X11))
& norm = index(status,host(X11)) ) )
& ! [X14,X15,X16] :
( ( setIn(X16,alive)
& elem(m_Ack(X16,X15),queue(host(X16)))
& leq(nbr_proc,index(pendack,host(X16)))
& elec_2 = index(status,host(X16))
& index(pendack,host(X16)) = host(X15) )
=> ~ ( setIn(X14,alive)
& host(X14) = index(ldr,host(X14))
& norm = index(status,host(X14)) ) )
& ! [X17,X18,X19] :
( ( ! [X20] :
( ( ~ leq(host(X19),X20)
& leq(s(zero),X20) )
=> ( setIn(X20,index(down,host(X19)))
| host(X18) = X20 ) )
& ~ leq(host(X19),host(X17))
& elem(m_Down(X18),queue(host(X19)))
& elec_1 = index(status,host(X19)) )
=> ~ ( setIn(X17,alive)
& host(X17) = index(ldr,host(X17))
& norm = index(status,host(X17)) ) )
& 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))) ) )
=> ( ( ! [X21] :
( ( ~ leq(host(X2),X21)
& leq(s(zero),X21) )
=> ( setIn(X21,index(down,host(X2)))
| host(X3) = X21 ) )
& index(status,host(X2)) = elec_1 )
=> ( leq(nbr_proc,host(X2))
=> ! [X22] :
( ~ setIn(host(X22),setEmpty)
=> ! [X23] :
( host(X2) = host(X23)
=> ! [X24] :
( host(X2) != host(X24)
=> ( ( setIn(X23,alive)
& setIn(X24,alive)
& host(X2) = host(X23)
& host(X24) = index(ldr,host(X24))
& norm = index(status,host(X24)) )
=> X23 = X24 ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f68]) ).
fof(f70,plain,
? [X0,X2,X3] :
( ? [X22] :
( ? [X23] :
( ? [X24] :
( X23 != X24
& setIn(X23,alive)
& setIn(X24,alive)
& host(X2) = host(X23)
& host(X24) = index(ldr,host(X24))
& norm = index(status,host(X24))
& host(X2) != host(X24) )
& host(X2) = host(X23) )
& ~ setIn(host(X22),setEmpty) )
& leq(nbr_proc,host(X2))
& ! [X21] :
( setIn(X21,index(down,host(X2)))
| host(X3) = X21
| leq(host(X2),X21)
| ~ leq(s(zero),X21) )
& 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] :
( ~ setIn(X6,alive)
| ~ setIn(X7,alive)
| X6 = X7
| host(X6) != host(X7) )
& ! [X8] :
( index(elid,host(X8)) = X8
| ( elec_1 != index(status,host(X8))
& elec_2 != index(status,host(X8)) )
| ~ setIn(X8,alive) )
& ! [X9,X10] :
( X9 = X10
| ~ setIn(X9,alive)
| ~ setIn(X10,alive)
| host(X9) != index(ldr,host(X9))
| norm != index(status,host(X9))
| norm != index(status,host(X10))
| host(X10) != index(ldr,host(X10)) )
& ! [X11,X12,X13] :
( ~ setIn(X11,alive)
| host(X11) != index(ldr,host(X11))
| norm != index(status,host(X11))
| ~ setIn(X13,alive)
| ~ elem(m_Down(X12),queue(host(X13)))
| ~ leq(nbr_proc,index(pendack,host(X13)))
| elec_2 != index(status,host(X13))
| index(pendack,host(X13)) != host(X12) )
& ! [X14,X15,X16] :
( ~ setIn(X14,alive)
| host(X14) != index(ldr,host(X14))
| norm != index(status,host(X14))
| ~ setIn(X16,alive)
| ~ elem(m_Ack(X16,X15),queue(host(X16)))
| ~ leq(nbr_proc,index(pendack,host(X16)))
| elec_2 != index(status,host(X16))
| index(pendack,host(X16)) != host(X15) )
& ! [X17,X18,X19] :
( ~ setIn(X17,alive)
| host(X17) != index(ldr,host(X17))
| norm != index(status,host(X17))
| ? [X20] :
( ~ setIn(X20,index(down,host(X19)))
& host(X18) != X20
& ~ leq(host(X19),X20)
& leq(s(zero),X20) )
| leq(host(X19),host(X17))
| ~ elem(m_Down(X18),queue(host(X19)))
| elec_1 != index(status,host(X19)) )
& queue(host(X2)) = cons(m_Down(X3),X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f71,plain,
? [X0,X2,X3] :
( ? [X22] :
( ? [X23] :
( ? [X24] :
( X23 != X24
& setIn(X23,alive)
& setIn(X24,alive)
& host(X2) = host(X23)
& host(X24) = index(ldr,host(X24))
& norm = index(status,host(X24))
& host(X2) != host(X24) )
& host(X2) = host(X23) )
& ~ setIn(host(X22),setEmpty) )
& leq(nbr_proc,host(X2))
& ! [X21] :
( setIn(X21,index(down,host(X2)))
| host(X3) = X21
| leq(host(X2),X21)
| ~ leq(s(zero),X21) )
& 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] :
( ~ setIn(X6,alive)
| ~ setIn(X7,alive)
| X6 = X7
| host(X6) != host(X7) )
& ! [X8] :
( index(elid,host(X8)) = X8
| ( elec_1 != index(status,host(X8))
& elec_2 != index(status,host(X8)) )
| ~ setIn(X8,alive) )
& ! [X9,X10] :
( X9 = X10
| ~ setIn(X9,alive)
| ~ setIn(X10,alive)
| host(X9) != index(ldr,host(X9))
| norm != index(status,host(X9))
| norm != index(status,host(X10))
| host(X10) != index(ldr,host(X10)) )
& ! [X11,X12,X13] :
( ~ setIn(X11,alive)
| host(X11) != index(ldr,host(X11))
| norm != index(status,host(X11))
| ~ setIn(X13,alive)
| ~ elem(m_Down(X12),queue(host(X13)))
| ~ leq(nbr_proc,index(pendack,host(X13)))
| elec_2 != index(status,host(X13))
| index(pendack,host(X13)) != host(X12) )
& ! [X14,X15,X16] :
( ~ setIn(X14,alive)
| host(X14) != index(ldr,host(X14))
| norm != index(status,host(X14))
| ~ setIn(X16,alive)
| ~ elem(m_Ack(X16,X15),queue(host(X16)))
| ~ leq(nbr_proc,index(pendack,host(X16)))
| elec_2 != index(status,host(X16))
| index(pendack,host(X16)) != host(X15) )
& ! [X17,X18,X19] :
( ~ setIn(X17,alive)
| host(X17) != index(ldr,host(X17))
| norm != index(status,host(X17))
| ? [X20] :
( ~ setIn(X20,index(down,host(X19)))
& host(X18) != X20
& ~ leq(host(X19),X20)
& leq(s(zero),X20) )
| leq(host(X19),host(X17))
| ~ elem(m_Down(X18),queue(host(X19)))
| elec_1 != index(status,host(X19)) )
& queue(host(X2)) = cons(m_Down(X3),X0) ),
inference(flattening,[],[f70]) ).
fof(f75,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(ennf_transformation,[],[f63]) ).
fof(f76,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(flattening,[],[f75]) ).
fof(f78,plain,
? [X0,X1,X2] :
( ? [X3] :
( ? [X4] :
( ? [X5] :
( X4 != X5
& setIn(X4,alive)
& setIn(X5,alive)
& host(X1) = host(X4)
& host(X5) = index(ldr,host(X5))
& norm = index(status,host(X5))
& host(X1) != host(X5) )
& host(X1) = host(X4) )
& ~ setIn(host(X3),setEmpty) )
& leq(nbr_proc,host(X1))
& ! [X6] :
( setIn(X6,index(down,host(X1)))
| host(X2) = X6
| leq(host(X1),X6)
| ~ leq(s(zero),X6) )
& 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)
& ! [X7,X8] :
( ~ leq(host(X7),host(X8))
| ~ elem(m_Ldr(X8),queue(host(X7))) )
& ! [X9,X10] :
( ~ setIn(X9,alive)
| ~ setIn(X10,alive)
| X9 = X10
| host(X9) != host(X10) )
& ! [X11] :
( index(elid,host(X11)) = X11
| ( elec_1 != index(status,host(X11))
& elec_2 != index(status,host(X11)) )
| ~ setIn(X11,alive) )
& ! [X12,X13] :
( X12 = X13
| ~ setIn(X12,alive)
| ~ setIn(X13,alive)
| host(X12) != index(ldr,host(X12))
| norm != index(status,host(X12))
| norm != index(status,host(X13))
| host(X13) != index(ldr,host(X13)) )
& ! [X14,X15,X16] :
( ~ setIn(X14,alive)
| host(X14) != index(ldr,host(X14))
| norm != index(status,host(X14))
| ~ setIn(X16,alive)
| ~ elem(m_Down(X15),queue(host(X16)))
| ~ leq(nbr_proc,index(pendack,host(X16)))
| elec_2 != index(status,host(X16))
| index(pendack,host(X16)) != host(X15) )
& ! [X17,X18,X19] :
( ~ setIn(X17,alive)
| host(X17) != index(ldr,host(X17))
| norm != index(status,host(X17))
| ~ setIn(X19,alive)
| ~ elem(m_Ack(X19,X18),queue(host(X19)))
| ~ leq(nbr_proc,index(pendack,host(X19)))
| elec_2 != index(status,host(X19))
| host(X18) != index(pendack,host(X19)) )
& ! [X20,X21,X22] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| ? [X23] :
( ~ setIn(X23,index(down,host(X22)))
& host(X21) != X23
& ~ leq(host(X22),X23)
& leq(s(zero),X23) )
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| elec_1 != index(status,host(X22)) )
& queue(host(X1)) = cons(m_Down(X2),X0) ),
inference(rectify,[],[f71]) ).
fof(f79,plain,
( sK4 != sK5
& setIn(sK4,alive)
& setIn(sK5,alive)
& host(sK1) = host(sK4)
& host(sK5) = index(ldr,host(sK5))
& norm = index(status,host(sK5))
& host(sK1) != host(sK5)
& host(sK1) = host(sK4)
& ~ setIn(host(sK3),setEmpty)
& leq(nbr_proc,host(sK1))
& ! [X6] :
( setIn(X6,index(down,host(sK1)))
| host(sK2) = X6
| leq(host(sK1),X6)
| ~ leq(s(zero),X6) )
& 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)
& ! [X7,X8] :
( ~ leq(host(X7),host(X8))
| ~ elem(m_Ldr(X8),queue(host(X7))) )
& ! [X9,X10] :
( ~ setIn(X9,alive)
| ~ setIn(X10,alive)
| X9 = X10
| host(X9) != host(X10) )
& ! [X11] :
( index(elid,host(X11)) = X11
| ( elec_1 != index(status,host(X11))
& elec_2 != index(status,host(X11)) )
| ~ setIn(X11,alive) )
& ! [X12,X13] :
( X12 = X13
| ~ setIn(X12,alive)
| ~ setIn(X13,alive)
| host(X12) != index(ldr,host(X12))
| norm != index(status,host(X12))
| norm != index(status,host(X13))
| host(X13) != index(ldr,host(X13)) )
& ! [X14,X15,X16] :
( ~ setIn(X14,alive)
| host(X14) != index(ldr,host(X14))
| norm != index(status,host(X14))
| ~ setIn(X16,alive)
| ~ elem(m_Down(X15),queue(host(X16)))
| ~ leq(nbr_proc,index(pendack,host(X16)))
| elec_2 != index(status,host(X16))
| index(pendack,host(X16)) != host(X15) )
& ! [X17,X18,X19] :
( ~ setIn(X17,alive)
| host(X17) != index(ldr,host(X17))
| norm != index(status,host(X17))
| ~ setIn(X19,alive)
| ~ elem(m_Ack(X19,X18),queue(host(X19)))
| ~ leq(nbr_proc,index(pendack,host(X19)))
| elec_2 != index(status,host(X19))
| host(X18) != index(pendack,host(X19)) )
& ! [X20,X21,X22] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| ( ~ setIn(sK6(X21,X22),index(down,host(X22)))
& host(X21) != sK6(X21,X22)
& ~ leq(host(X22),sK6(X21,X22))
& leq(s(zero),sK6(X21,X22)) )
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| elec_1 != index(status,host(X22)) )
& queue(host(sK1)) = cons(m_Down(sK2),sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X23,sK6(X21,X22))],[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(f91,plain,
queue(host(sK1)) = cons(m_Down(sK2),sK0),
inference(cnf_transformation,[],[f79]) ).
fof(f92,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| leq(s(zero),sK6(X21,X22))
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| elec_1 != index(status,host(X22)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f93,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| ~ leq(host(X22),sK6(X21,X22))
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| elec_1 != index(status,host(X22)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f94,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| host(X21) != sK6(X21,X22)
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| elec_1 != index(status,host(X22)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f95,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| norm != index(status,host(X20))
| ~ setIn(sK6(X21,X22),index(down,host(X22)))
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| elec_1 != index(status,host(X22)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f100,plain,
! [X11] :
( index(elid,host(X11)) = X11
| elec_1 != index(status,host(X11))
| ~ setIn(X11,alive) ),
inference(cnf_transformation,[],[f79]) ).
fof(f101,plain,
! [X10,X9] :
( host(X9) != host(X10)
| ~ setIn(X10,alive)
| X9 = X10
| ~ setIn(X9,alive) ),
inference(cnf_transformation,[],[f79]) ).
fof(f103,plain,
setIn(sK1,alive),
inference(cnf_transformation,[],[f79]) ).
fof(f104,plain,
~ leq(host(sK1),host(sK2)),
inference(cnf_transformation,[],[f79]) ).
fof(f107,plain,
elec_1 = index(status,host(sK1)),
inference(cnf_transformation,[],[f79]) ).
fof(f108,plain,
! [X6] :
( setIn(X6,index(down,host(sK1)))
| host(sK2) = X6
| leq(host(sK1),X6)
| ~ leq(s(zero),X6) ),
inference(cnf_transformation,[],[f79]) ).
fof(f109,plain,
leq(nbr_proc,host(sK1)),
inference(cnf_transformation,[],[f79]) ).
fof(f111,plain,
host(sK1) = host(sK4),
inference(cnf_transformation,[],[f79]) ).
fof(f112,plain,
host(sK1) != host(sK5),
inference(cnf_transformation,[],[f79]) ).
fof(f113,plain,
norm = index(status,host(sK5)),
inference(cnf_transformation,[],[f79]) ).
fof(f114,plain,
host(sK5) = index(ldr,host(sK5)),
inference(cnf_transformation,[],[f79]) ).
fof(f116,plain,
setIn(sK5,alive),
inference(cnf_transformation,[],[f79]) ).
fof(f117,plain,
setIn(sK4,alive),
inference(cnf_transformation,[],[f79]) ).
fof(f127,plain,
! [X2,X0,X1] :
( elem(X0,cons(X1,X2))
| X0 != X1 ),
inference(cnf_transformation,[],[f83]) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(cnf_transformation,[],[f76]) ).
fof(f131,plain,
! [X0,X1] :
( ~ leq(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f85]) ).
fof(f133,plain,
! [X0,X1] :
( leq(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f85]) ).
fof(f134,plain,
! [X0,X1] :
( leq(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f135,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[],[f60]) ).
fof(f145,plain,
! [X0] : leq(host(X0),nbr_proc),
inference(cnf_transformation,[],[f5]) ).
fof(f163,definition,
~ sP8(host(sK1)),
introduced(definition,[new_symbols(definition,[sP8])],[inequality_splitting_name_introduction]) ).
fof(f164,plain,
sP8(host(sK5)),
inference(inequality_splitting,[],[f112,f163]) ).
fof(f171,definition,
~ sP13(elec_1),
introduced(definition,[new_symbols(definition,[sP13])],[inequality_splitting_name_introduction]) ).
fof(f172,plain,
! [X11] :
( index(elid,host(X11)) = X11
| sP13(index(status,host(X11)))
| ~ setIn(X11,alive) ),
inference(inequality_splitting,[],[f100,f171]) ).
fof(f184,definition,
~ sP21(norm),
introduced(definition,[new_symbols(definition,[sP21])],[inequality_splitting_name_introduction]) ).
fof(f185,definition,
~ sP22(elec_1),
introduced(definition,[new_symbols(definition,[sP22])],[inequality_splitting_name_introduction]) ).
fof(f186,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| sP21(index(status,host(X20)))
| ~ setIn(sK6(X21,X22),index(down,host(X22)))
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| sP22(index(status,host(X22))) ),
inference(inequality_splitting,[],[f95,f185,f184]) ).
fof(f187,definition,
~ sP23(norm),
introduced(definition,[new_symbols(definition,[sP23])],[inequality_splitting_name_introduction]) ).
fof(f188,definition,
~ sP24(elec_1),
introduced(definition,[new_symbols(definition,[sP24])],[inequality_splitting_name_introduction]) ).
fof(f189,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| sP23(index(status,host(X20)))
| host(X21) != sK6(X21,X22)
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| sP24(index(status,host(X22))) ),
inference(inequality_splitting,[],[f94,f188,f187]) ).
fof(f190,definition,
~ sP25(norm),
introduced(definition,[new_symbols(definition,[sP25])],[inequality_splitting_name_introduction]) ).
fof(f191,definition,
~ sP26(elec_1),
introduced(definition,[new_symbols(definition,[sP26])],[inequality_splitting_name_introduction]) ).
fof(f192,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| sP25(index(status,host(X20)))
| ~ leq(host(X22),sK6(X21,X22))
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| sP26(index(status,host(X22))) ),
inference(inequality_splitting,[],[f93,f191,f190]) ).
fof(f193,definition,
~ sP27(norm),
introduced(definition,[new_symbols(definition,[sP27])],[inequality_splitting_name_introduction]) ).
fof(f194,definition,
~ sP28(elec_1),
introduced(definition,[new_symbols(definition,[sP28])],[inequality_splitting_name_introduction]) ).
fof(f195,plain,
! [X21,X22,X20] :
( ~ setIn(X20,alive)
| host(X20) != index(ldr,host(X20))
| sP27(index(status,host(X20)))
| leq(s(zero),sK6(X21,X22))
| leq(host(X22),host(X20))
| ~ elem(m_Down(X21),queue(host(X22)))
| sP28(index(status,host(X22))) ),
inference(inequality_splitting,[],[f92,f194,f193]) ).
fof(f209,plain,
! [X2,X1] : elem(X1,cons(X1,X2)),
inference(equality_resolution,[],[f127]) ).
fof(f211,plain,
! [X1] : leq(X1,X1),
inference(equality_resolution,[],[f133]) ).
fof(f220,plain,
! [X21,X22] :
( ~ setIn(sK6(X21,X22),index(down,host(X22)))
| ~ elem(m_Down(X21),queue(host(X22)))
| sP37(X22) ),
inference(cnf_transformation,[],[f220_D]) ).
fof(f220_D,definition,
! [X22] :
( ! [X21] :
( ~ setIn(sK6(X21,X22),index(down,host(X22)))
| ~ elem(m_Down(X21),queue(host(X22))) )
<=> ~ sP37(X22) ),
introduced(definition,[new_symbols(definition,[sP37])],[general_splitting_component_introduction]) ).
fof(f221,plain,
! [X22,X20] :
( host(X20) != index(ldr,host(X20))
| ~ setIn(X20,alive)
| sP21(index(status,host(X20)))
| leq(host(X22),host(X20))
| sP22(index(status,host(X22)))
| ~ sP37(X22) ),
inference(general_splitting,[],[f186,f220_D]) ).
fof(f222,plain,
! [X21,X22] :
( host(X21) != sK6(X21,X22)
| ~ elem(m_Down(X21),queue(host(X22)))
| sP38(X22) ),
inference(cnf_transformation,[],[f222_D]) ).
fof(f222_D,definition,
! [X22] :
( ! [X21] :
( host(X21) != sK6(X21,X22)
| ~ elem(m_Down(X21),queue(host(X22))) )
<=> ~ sP38(X22) ),
introduced(definition,[new_symbols(definition,[sP38])],[general_splitting_component_introduction]) ).
fof(f223,plain,
! [X22,X20] :
( host(X20) != index(ldr,host(X20))
| ~ setIn(X20,alive)
| sP23(index(status,host(X20)))
| leq(host(X22),host(X20))
| sP24(index(status,host(X22)))
| ~ sP38(X22) ),
inference(general_splitting,[],[f189,f222_D]) ).
fof(f224,plain,
! [X21,X22] :
( ~ leq(host(X22),sK6(X21,X22))
| ~ elem(m_Down(X21),queue(host(X22)))
| sP39(X22) ),
inference(cnf_transformation,[],[f224_D]) ).
fof(f224_D,definition,
! [X22] :
( ! [X21] :
( ~ leq(host(X22),sK6(X21,X22))
| ~ elem(m_Down(X21),queue(host(X22))) )
<=> ~ sP39(X22) ),
introduced(definition,[new_symbols(definition,[sP39])],[general_splitting_component_introduction]) ).
fof(f225,plain,
! [X22,X20] :
( host(X20) != index(ldr,host(X20))
| ~ setIn(X20,alive)
| sP25(index(status,host(X20)))
| leq(host(X22),host(X20))
| sP26(index(status,host(X22)))
| ~ sP39(X22) ),
inference(general_splitting,[],[f192,f224_D]) ).
fof(f226,plain,
! [X21,X22] :
( ~ elem(m_Down(X21),queue(host(X22)))
| leq(s(zero),sK6(X21,X22))
| sP40(X22) ),
inference(cnf_transformation,[],[f226_D]) ).
fof(f226_D,definition,
! [X22] :
( ! [X21] :
( ~ elem(m_Down(X21),queue(host(X22)))
| leq(s(zero),sK6(X21,X22)) )
<=> ~ sP40(X22) ),
introduced(definition,[new_symbols(definition,[sP40])],[general_splitting_component_introduction]) ).
fof(f227,plain,
! [X22,X20] :
( host(X20) != index(ldr,host(X20))
| ~ setIn(X20,alive)
| sP27(index(status,host(X20)))
| leq(host(X22),host(X20))
| sP28(index(status,host(X22)))
| ~ sP40(X22) ),
inference(general_splitting,[],[f195,f226_D]) ).
fof(f270,plain,
( ~ leq(host(sK1),nbr_proc)
| nbr_proc = host(sK1) ),
inference(resolution,[],[f109,f131]) ).
fof(f272,plain,
nbr_proc = host(sK1),
inference(forward_subsumption_resolution,[],[f270,f145]) ).
fof(f274,plain,
! [X0] : leq(host(X0),host(sK1)),
inference(superposition,[],[f145,f272]) ).
fof(f281,plain,
~ sP13(index(status,host(sK1))),
inference(superposition,[],[f171,f107]) ).
fof(f282,plain,
~ sP22(index(status,host(sK1))),
inference(superposition,[],[f185,f107]) ).
fof(f283,plain,
~ sP24(index(status,host(sK1))),
inference(superposition,[],[f188,f107]) ).
fof(f284,plain,
~ sP26(index(status,host(sK1))),
inference(superposition,[],[f191,f107]) ).
fof(f285,plain,
~ sP28(index(status,host(sK1))),
inference(superposition,[],[f194,f107]) ).
fof(f291,plain,
elem(m_Down(sK2),queue(host(sK1))),
inference(superposition,[],[f209,f91]) ).
fof(f294,plain,
! [X0] :
( host(X0) != host(sK1)
| ~ setIn(sK4,alive)
| sK4 = X0
| ~ setIn(X0,alive) ),
inference(superposition,[],[f101,f111]) ).
fof(f297,plain,
! [X0] :
( host(X0) != host(sK1)
| sK4 = X0
| ~ setIn(X0,alive) ),
inference(forward_subsumption_resolution,[],[f294,f117]) ).
fof(f299,plain,
( sK4 = index(elid,host(sK1))
| sP13(index(status,host(sK1)))
| ~ setIn(sK4,alive) ),
inference(superposition,[],[f172,f111]) ).
fof(f300,plain,
( sK4 = index(elid,host(sK1))
| ~ setIn(sK4,alive) ),
inference(forward_subsumption_resolution,[],[f299,f281]) ).
fof(f301,plain,
sK4 = index(elid,host(sK1)),
inference(forward_subsumption_resolution,[],[f300,f117]) ).
fof(f309,plain,
! [X0,X1] :
( ~ elem(m_Down(X0),queue(host(X1)))
| sP39(X1)
| leq(sK6(X0,X1),host(X1)) ),
inference(resolution,[],[f224,f134]) ).
fof(f310,plain,
! [X0] :
( ~ leq(host(sK1),sK6(X0,sK4))
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP39(sK4) ),
inference(superposition,[],[f224,f111]) ).
fof(f311,plain,
! [X0] :
( ~ leq(host(sK1),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP39(sK4) ),
inference(forward_demodulation,[],[f310,f301]) ).
fof(f312,plain,
! [X0] :
( sP39(index(elid,host(sK1)))
| ~ leq(host(sK1),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1))) ),
inference(forward_demodulation,[],[f311,f301]) ).
fof(f314,definition,
( spl41_11
<=> ! [X0] :
( ~ leq(host(sK1),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1))) ) ),
introduced(definition,[new_symbols(definition,[spl41_11])],[avatar_definition]) ).
fof(f315,plain,
( ! [X0] :
( ~ leq(host(sK1),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl41_11 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f317,definition,
( spl41_12
<=> sP39(index(elid,host(sK1))) ),
introduced(definition,[new_symbols(definition,[spl41_12])],[avatar_definition]) ).
fof(f319,plain,
( sP39(index(elid,host(sK1)))
| ~ spl41_12 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f320,plain,
( spl41_11
| spl41_12 ),
inference(avatar_split_clause,[],[f312,f317,f314]) ).
fof(f321,plain,
( leq(s(zero),sK6(sK2,sK1))
| sP40(sK1) ),
inference(resolution,[],[f226,f291]) ).
fof(f322,plain,
! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| leq(s(zero),sK6(X0,sK4))
| sP40(sK4) ),
inference(superposition,[],[f226,f111]) ).
fof(f323,plain,
! [X0] :
( leq(s(zero),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP40(sK4) ),
inference(forward_demodulation,[],[f322,f301]) ).
fof(f325,definition,
( spl41_13
<=> sP40(sK1) ),
introduced(definition,[new_symbols(definition,[spl41_13])],[avatar_definition]) ).
fof(f326,plain,
( ~ sP40(sK1)
| spl41_13 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f327,plain,
( sP40(sK1)
| ~ spl41_13 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f329,definition,
( spl41_14
<=> leq(s(zero),sK6(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_14])],[avatar_definition]) ).
fof(f331,plain,
( leq(s(zero),sK6(sK2,sK1))
| ~ spl41_14 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,plain,
( spl41_13
| spl41_14 ),
inference(avatar_split_clause,[],[f321,f329,f325]) ).
fof(f333,plain,
! [X0] :
( sP40(index(elid,host(sK1)))
| leq(s(zero),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1))) ),
inference(forward_demodulation,[],[f323,f301]) ).
fof(f335,definition,
( spl41_15
<=> ! [X0] :
( leq(s(zero),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1))) ) ),
introduced(definition,[new_symbols(definition,[spl41_15])],[avatar_definition]) ).
fof(f336,plain,
( ! [X0] :
( leq(s(zero),sK6(X0,index(elid,host(sK1))))
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl41_15 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f338,definition,
( spl41_16
<=> sP40(index(elid,host(sK1))) ),
introduced(definition,[new_symbols(definition,[spl41_16])],[avatar_definition]) ).
fof(f340,plain,
( sP40(index(elid,host(sK1)))
| ~ spl41_16 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f341,plain,
( spl41_15
| spl41_16 ),
inference(avatar_split_clause,[],[f333,f338,f335]) ).
fof(f374,plain,
! [X0] :
( ~ setIn(sK6(X0,sK4),index(down,host(sK1)))
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP37(sK4) ),
inference(superposition,[],[f220,f111]) ).
fof(f375,plain,
! [X0] :
( ~ setIn(sK6(X0,index(elid,host(sK1))),index(down,host(sK1)))
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP37(sK4) ),
inference(forward_demodulation,[],[f374,f301]) ).
fof(f376,plain,
! [X0] :
( sP37(index(elid,host(sK1)))
| ~ setIn(sK6(X0,index(elid,host(sK1))),index(down,host(sK1)))
| ~ elem(m_Down(X0),queue(host(sK1))) ),
inference(forward_demodulation,[],[f375,f301]) ).
fof(f378,definition,
( spl41_20
<=> ! [X0] :
( ~ setIn(sK6(X0,index(elid,host(sK1))),index(down,host(sK1)))
| ~ elem(m_Down(X0),queue(host(sK1))) ) ),
introduced(definition,[new_symbols(definition,[spl41_20])],[avatar_definition]) ).
fof(f379,plain,
( ! [X0] :
( ~ setIn(sK6(X0,index(elid,host(sK1))),index(down,host(sK1)))
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl41_20 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f381,definition,
( spl41_21
<=> sP37(index(elid,host(sK1))) ),
introduced(definition,[new_symbols(definition,[spl41_21])],[avatar_definition]) ).
fof(f383,plain,
( sP37(index(elid,host(sK1)))
| ~ spl41_21 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f384,plain,
( spl41_20
| spl41_21 ),
inference(avatar_split_clause,[],[f376,f381,f378]) ).
fof(f388,plain,
! [X0] :
( host(sK2) = sK6(X0,sK1)
| leq(host(sK1),sK6(X0,sK1))
| ~ leq(s(zero),sK6(X0,sK1))
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP37(sK1) ),
inference(resolution,[],[f108,f220]) ).
fof(f390,definition,
( spl41_22
<=> sP37(sK1) ),
introduced(definition,[new_symbols(definition,[spl41_22])],[avatar_definition]) ).
fof(f391,plain,
( ~ sP37(sK1)
| spl41_22 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f392,plain,
( sP37(sK1)
| ~ spl41_22 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f394,definition,
( spl41_23
<=> ! [X0] :
( host(sK2) = sK6(X0,sK1)
| ~ elem(m_Down(X0),queue(host(sK1)))
| ~ leq(s(zero),sK6(X0,sK1))
| leq(host(sK1),sK6(X0,sK1)) ) ),
introduced(definition,[new_symbols(definition,[spl41_23])],[avatar_definition]) ).
fof(f395,plain,
( ! [X0] :
( ~ leq(s(zero),sK6(X0,sK1))
| ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK6(X0,sK1)
| leq(host(sK1),sK6(X0,sK1)) )
| ~ spl41_23 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f396,plain,
( spl41_22
| spl41_23 ),
inference(avatar_split_clause,[],[f388,f394,f390]) ).
fof(f398,plain,
! [X0] :
( host(sK5) != host(sK5)
| ~ setIn(sK5,alive)
| sP21(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP22(index(status,host(X0)))
| ~ sP37(X0) ),
inference(superposition,[],[f221,f114]) ).
fof(f399,plain,
! [X0] :
( ~ setIn(sK5,alive)
| sP21(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP22(index(status,host(X0)))
| ~ sP37(X0) ),
inference(trivial_inequality_removal,[],[f398]) ).
fof(f400,plain,
! [X0] :
( sP21(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP22(index(status,host(X0)))
| ~ sP37(X0) ),
inference(forward_subsumption_resolution,[],[f399,f116]) ).
fof(f401,plain,
! [X0] :
( sP21(norm)
| leq(host(X0),host(sK5))
| sP22(index(status,host(X0)))
| ~ sP37(X0) ),
inference(forward_demodulation,[],[f400,f113]) ).
fof(f402,plain,
! [X0] :
( sP22(index(status,host(X0)))
| leq(host(X0),host(sK5))
| ~ sP37(X0) ),
inference(forward_subsumption_resolution,[],[f401,f184]) ).
fof(f419,plain,
! [X0] :
( host(sK5) != host(sK5)
| ~ setIn(sK5,alive)
| sP23(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP24(index(status,host(X0)))
| ~ sP38(X0) ),
inference(superposition,[],[f223,f114]) ).
fof(f420,plain,
! [X0] :
( ~ setIn(sK5,alive)
| sP23(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP24(index(status,host(X0)))
| ~ sP38(X0) ),
inference(trivial_inequality_removal,[],[f419]) ).
fof(f421,plain,
! [X0] :
( sP23(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP24(index(status,host(X0)))
| ~ sP38(X0) ),
inference(forward_subsumption_resolution,[],[f420,f116]) ).
fof(f422,plain,
! [X0] :
( sP23(norm)
| leq(host(X0),host(sK5))
| sP24(index(status,host(X0)))
| ~ sP38(X0) ),
inference(forward_demodulation,[],[f421,f113]) ).
fof(f423,plain,
! [X0] :
( sP24(index(status,host(X0)))
| leq(host(X0),host(sK5))
| ~ sP38(X0) ),
inference(forward_subsumption_resolution,[],[f422,f187]) ).
fof(f425,plain,
! [X0] :
( host(sK5) != host(sK5)
| ~ setIn(sK5,alive)
| sP25(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP26(index(status,host(X0)))
| ~ sP39(X0) ),
inference(superposition,[],[f225,f114]) ).
fof(f426,plain,
! [X0] :
( ~ setIn(sK5,alive)
| sP25(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP26(index(status,host(X0)))
| ~ sP39(X0) ),
inference(trivial_inequality_removal,[],[f425]) ).
fof(f427,plain,
! [X0] :
( sP25(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP26(index(status,host(X0)))
| ~ sP39(X0) ),
inference(forward_subsumption_resolution,[],[f426,f116]) ).
fof(f428,plain,
! [X0] :
( sP25(norm)
| leq(host(X0),host(sK5))
| sP26(index(status,host(X0)))
| ~ sP39(X0) ),
inference(forward_demodulation,[],[f427,f113]) ).
fof(f429,plain,
! [X0] :
( sP26(index(status,host(X0)))
| leq(host(X0),host(sK5))
| ~ sP39(X0) ),
inference(forward_subsumption_resolution,[],[f428,f190]) ).
fof(f433,plain,
! [X0] :
( host(sK5) != host(sK5)
| ~ setIn(sK5,alive)
| sP27(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP28(index(status,host(X0)))
| ~ sP40(X0) ),
inference(superposition,[],[f227,f114]) ).
fof(f434,plain,
! [X0] :
( ~ setIn(sK5,alive)
| sP27(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP28(index(status,host(X0)))
| ~ sP40(X0) ),
inference(trivial_inequality_removal,[],[f433]) ).
fof(f435,plain,
! [X0] :
( sP27(index(status,host(sK5)))
| leq(host(X0),host(sK5))
| sP28(index(status,host(X0)))
| ~ sP40(X0) ),
inference(forward_subsumption_resolution,[],[f434,f116]) ).
fof(f436,plain,
! [X0] :
( sP27(norm)
| leq(host(X0),host(sK5))
| sP28(index(status,host(X0)))
| ~ sP40(X0) ),
inference(forward_demodulation,[],[f435,f113]) ).
fof(f437,plain,
! [X0] :
( sP28(index(status,host(X0)))
| leq(host(X0),host(sK5))
| ~ sP40(X0) ),
inference(forward_subsumption_resolution,[],[f436,f193]) ).
fof(f508,plain,
( sK1 = sK4
| ~ setIn(sK1,alive) ),
inference(equality_resolution,[],[f297]) ).
fof(f510,plain,
sK1 = sK4,
inference(forward_subsumption_resolution,[],[f508,f103]) ).
fof(f512,plain,
sK1 = index(elid,host(sK1)),
inference(superposition,[],[f301,f510]) ).
fof(f519,plain,
( leq(host(sK1),host(sK5))
| ~ sP37(sK1) ),
inference(resolution,[],[f402,f282]) ).
fof(f525,plain,
( leq(host(sK1),host(sK5))
| ~ spl41_22 ),
inference(forward_subsumption_resolution,[],[f519,f392]) ).
fof(f528,plain,
( ~ leq(host(sK5),host(sK1))
| host(sK1) = host(sK5)
| ~ spl41_22 ),
inference(resolution,[],[f525,f131]) ).
fof(f530,plain,
( host(sK1) = host(sK5)
| ~ spl41_22 ),
inference(forward_subsumption_resolution,[],[f528,f274]) ).
fof(f532,plain,
( sP24(index(status,host(sK1)))
| leq(host(sK1),host(sK5))
| ~ sP38(sK4) ),
inference(superposition,[],[f423,f111]) ).
fof(f538,plain,
( sP8(host(sK1))
| ~ spl41_22 ),
inference(superposition,[],[f164,f530]) ).
fof(f595,plain,
( $false
| ~ spl41_22 ),
inference(forward_subsumption_resolution,[],[f538,f163]) ).
fof(f596,plain,
~ spl41_22,
inference(avatar_contradiction_clause,[],[f595]) ).
fof(f612,plain,
( leq(host(sK1),host(sK5))
| ~ sP38(sK4) ),
inference(forward_subsumption_resolution,[],[f532,f283]) ).
fof(f614,definition,
( spl41_38
<=> sP38(sK1) ),
introduced(definition,[new_symbols(definition,[spl41_38])],[avatar_definition]) ).
fof(f616,plain,
( ~ sP38(sK1)
| spl41_38 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f618,definition,
( spl41_39
<=> leq(host(sK1),host(sK5)) ),
introduced(definition,[new_symbols(definition,[spl41_39])],[avatar_definition]) ).
fof(f620,plain,
( leq(host(sK1),host(sK5))
| ~ spl41_39 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f623,plain,
( ~ sP38(index(elid,host(sK1)))
| leq(host(sK1),host(sK5)) ),
inference(forward_demodulation,[],[f612,f301]) ).
fof(f625,plain,
( ~ sP38(sK1)
| leq(host(sK1),host(sK5)) ),
inference(forward_demodulation,[],[f623,f512]) ).
fof(f626,plain,
( spl41_39
| ~ spl41_38 ),
inference(avatar_split_clause,[],[f625,f614,f618]) ).
fof(f628,plain,
( sP26(index(status,host(sK1)))
| leq(host(sK1),host(sK5))
| ~ sP39(sK4) ),
inference(superposition,[],[f429,f111]) ).
fof(f632,plain,
( leq(host(sK1),host(sK5))
| ~ sP39(sK4) ),
inference(forward_subsumption_resolution,[],[f628,f284]) ).
fof(f634,definition,
( spl41_40
<=> sP39(sK1) ),
introduced(definition,[new_symbols(definition,[spl41_40])],[avatar_definition]) ).
fof(f636,plain,
( ~ sP39(sK1)
| spl41_40 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f639,plain,
( ~ sP39(index(elid,host(sK1)))
| leq(host(sK1),host(sK5)) ),
inference(forward_demodulation,[],[f632,f301]) ).
fof(f641,plain,
( ~ sP39(sK1)
| leq(host(sK1),host(sK5)) ),
inference(forward_demodulation,[],[f639,f512]) ).
fof(f642,plain,
( spl41_39
| ~ spl41_40 ),
inference(avatar_split_clause,[],[f641,f634,f618]) ).
fof(f643,plain,
( leq(host(sK1),host(sK5))
| ~ sP40(sK1) ),
inference(resolution,[],[f437,f285]) ).
fof(f649,plain,
( leq(host(sK1),host(sK5))
| ~ spl41_13 ),
inference(forward_subsumption_resolution,[],[f643,f327]) ).
fof(f652,plain,
( spl41_39
| ~ spl41_13 ),
inference(avatar_split_clause,[],[f649,f325,f618]) ).
fof(f657,plain,
( sP39(sK1)
| leq(sK6(sK2,sK1),host(sK1)) ),
inference(resolution,[],[f309,f291]) ).
fof(f664,plain,
( leq(sK6(sK2,sK1),host(sK1))
| spl41_40 ),
inference(forward_subsumption_resolution,[],[f657,f636]) ).
fof(f672,plain,
( ! [X0] :
( leq(X0,sK6(sK2,sK1))
| ~ leq(X0,s(zero)) )
| ~ spl41_14 ),
inference(resolution,[],[f331,f130]) ).
fof(f683,plain,
( ! [X0] :
( ~ leq(host(sK1),sK6(X0,sK1))
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl41_11 ),
inference(superposition,[],[f315,f512]) ).
fof(f689,plain,
( ~ leq(host(sK1),sK6(sK2,sK1))
| host(sK1) = sK6(sK2,sK1)
| spl41_40 ),
inference(resolution,[],[f664,f131]) ).
fof(f692,definition,
( spl41_43
<=> host(sK1) = sK6(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl41_43])],[avatar_definition]) ).
fof(f694,plain,
( host(sK1) = sK6(sK2,sK1)
| ~ spl41_43 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f696,definition,
( spl41_44
<=> leq(host(sK1),sK6(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl41_44])],[avatar_definition]) ).
fof(f698,plain,
( ~ leq(host(sK1),sK6(sK2,sK1))
| spl41_44 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f699,plain,
( spl41_43
| ~ spl41_44
| spl41_40 ),
inference(avatar_split_clause,[],[f689,f634,f696,f692]) ).
fof(f712,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK6(X0,index(elid,host(sK1)))
| leq(host(sK1),sK6(X0,index(elid,host(sK1))))
| ~ leq(s(zero),sK6(X0,index(elid,host(sK1)))) )
| ~ spl41_20 ),
inference(resolution,[],[f379,f108]) ).
fof(f718,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK6(X0,index(elid,host(sK1)))
| ~ leq(s(zero),sK6(X0,index(elid,host(sK1)))) )
| ~ spl41_11
| ~ spl41_20 ),
inference(forward_subsumption_resolution,[],[f712,f315]) ).
fof(f719,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK6(X0,index(elid,host(sK1))) )
| ~ spl41_11
| ~ spl41_15
| ~ spl41_20 ),
inference(forward_subsumption_resolution,[],[f718,f336]) ).
fof(f720,plain,
( ! [X0] :
( ~ elem(m_Down(X0),queue(host(sK1)))
| host(sK2) = sK6(X0,sK1) )
| ~ spl41_11
| ~ spl41_15
| ~ spl41_20 ),
inference(forward_demodulation,[],[f719,f512]) ).
fof(f730,plain,
( ~ elem(m_Down(sK2),queue(host(sK1)))
| host(sK2) = sK6(sK2,sK1)
| leq(host(sK1),sK6(sK2,sK1))
| ~ spl41_14
| ~ spl41_23 ),
inference(resolution,[],[f395,f331]) ).
fof(f792,plain,
( host(sK2) = sK6(sK2,sK1)
| ~ spl41_11
| ~ spl41_15
| ~ spl41_20 ),
inference(resolution,[],[f720,f291]) ).
fof(f794,plain,
( ~ leq(host(sK1),sK6(sK2,sK1))
| ~ spl41_11
| ~ spl41_15
| ~ spl41_20 ),
inference(superposition,[],[f104,f792]) ).
fof(f1008,plain,
( sP37(sK1)
| ~ spl41_21 ),
inference(forward_demodulation,[],[f383,f512]) ).
fof(f1013,plain,
( $false
| ~ spl41_21
| spl41_22 ),
inference(forward_subsumption_resolution,[],[f1008,f391]) ).
fof(f1014,plain,
( ~ spl41_21
| spl41_22 ),
inference(avatar_contradiction_clause,[],[f1013]) ).
fof(f1019,plain,
( sP39(sK1)
| ~ spl41_12 ),
inference(forward_demodulation,[],[f319,f512]) ).
fof(f1023,plain,
( host(sK2) = sK6(sK2,sK1)
| leq(host(sK1),sK6(sK2,sK1))
| ~ spl41_14
| ~ spl41_23 ),
inference(forward_subsumption_resolution,[],[f730,f291]) ).
fof(f1025,plain,
( $false
| ~ spl41_12
| spl41_40 ),
inference(forward_subsumption_resolution,[],[f1019,f636]) ).
fof(f1026,plain,
( ~ spl41_12
| spl41_40 ),
inference(avatar_contradiction_clause,[],[f1025]) ).
fof(f1028,plain,
( host(sK2) = sK6(sK2,sK1)
| ~ spl41_14
| ~ spl41_23
| spl41_44 ),
inference(forward_subsumption_resolution,[],[f1023,f698]) ).
fof(f1033,plain,
( sP40(sK1)
| ~ spl41_16 ),
inference(forward_demodulation,[],[f340,f512]) ).
fof(f1035,plain,
( $false
| spl41_13
| ~ spl41_16 ),
inference(forward_subsumption_resolution,[],[f1033,f326]) ).
fof(f1036,plain,
( spl41_13
| ~ spl41_16 ),
inference(avatar_contradiction_clause,[],[f1035]) ).
fof(f1040,plain,
( ~ leq(host(sK5),host(sK1))
| host(sK1) = host(sK5)
| ~ spl41_39 ),
inference(resolution,[],[f620,f131]) ).
fof(f1042,plain,
( host(sK1) = host(sK5)
| ~ spl41_39 ),
inference(forward_subsumption_resolution,[],[f1040,f274]) ).
fof(f1080,plain,
( sP8(host(sK1))
| ~ spl41_39 ),
inference(superposition,[],[f164,f1042]) ).
fof(f1128,plain,
( $false
| ~ spl41_39 ),
inference(forward_subsumption_resolution,[],[f1080,f163]) ).
fof(f1129,plain,
~ spl41_39,
inference(avatar_contradiction_clause,[],[f1128]) ).
fof(f1149,plain,
( ! [X0] :
( sK6(sK2,sK1) = sK6(X0,sK1)
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_44 ),
inference(forward_demodulation,[],[f720,f1028]) ).
fof(f1188,plain,
( ! [X0] :
( host(X0) != sK6(sK2,sK1)
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP38(sK1)
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_44 ),
inference(superposition,[],[f222,f1149]) ).
fof(f1189,plain,
( ! [X0] :
( host(X0) != sK6(sK2,sK1)
| ~ elem(m_Down(X0),queue(host(sK1)))
| sP38(sK1) )
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_44 ),
inference(duplicate_literal_removal,[],[f1188]) ).
fof(f1193,plain,
( ! [X0] :
( host(X0) != sK6(sK2,sK1)
| ~ elem(m_Down(X0),queue(host(sK1))) )
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_38
| spl41_44 ),
inference(forward_subsumption_resolution,[],[f1189,f616]) ).
fof(f1264,plain,
( ~ leq(s(zero),s(zero))
| ~ elem(m_Down(sK2),queue(host(sK1)))
| host(sK2) = sK6(sK2,sK1)
| leq(host(sK1),sK6(sK2,sK1))
| ~ spl41_14
| ~ spl41_23 ),
inference(resolution,[],[f672,f395]) ).
fof(f1267,plain,
( ~ leq(s(zero),s(zero))
| ~ elem(m_Down(sK2),queue(host(sK1)))
| leq(host(sK1),sK6(sK2,sK1))
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_38
| spl41_44 ),
inference(forward_subsumption_resolution,[],[f1264,f1193]) ).
fof(f1268,plain,
( ~ leq(s(zero),s(zero))
| ~ elem(m_Down(sK2),queue(host(sK1)))
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_38
| spl41_44 ),
inference(forward_subsumption_resolution,[],[f1267,f683]) ).
fof(f1269,plain,
( ~ elem(m_Down(sK2),queue(host(sK1)))
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_38
| spl41_44 ),
inference(forward_subsumption_resolution,[],[f1268,f211]) ).
fof(f1270,plain,
( $false
| ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_38
| spl41_44 ),
inference(forward_subsumption_resolution,[],[f1269,f291]) ).
fof(f1271,plain,
( ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_38
| spl41_44 ),
inference(avatar_contradiction_clause,[],[f1270]) ).
fof(f1278,plain,
( ~ leq(host(sK1),host(sK1))
| ~ spl41_11
| ~ spl41_15
| ~ spl41_20
| ~ spl41_43 ),
inference(forward_demodulation,[],[f794,f694]) ).
fof(f1285,plain,
( $false
| ~ spl41_11
| ~ spl41_15
| ~ spl41_20
| ~ spl41_43 ),
inference(forward_subsumption_resolution,[],[f1278,f135]) ).
fof(f1286,plain,
( ~ spl41_11
| ~ spl41_15
| ~ spl41_20
| ~ spl41_43 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
cnf(s7,plain,
( spl41_11
| spl41_12 ),
inference(sat_conversion,[],[f320]) ).
cnf(s8,plain,
( spl41_13
| spl41_14 ),
inference(sat_conversion,[],[f332]) ).
cnf(s9,plain,
( spl41_15
| spl41_16 ),
inference(sat_conversion,[],[f341]) ).
cnf(s14,plain,
( spl41_20
| spl41_21 ),
inference(sat_conversion,[],[f384]) ).
cnf(s15,plain,
( spl41_22
| spl41_23 ),
inference(sat_conversion,[],[f396]) ).
cnf(s23,plain,
~ spl41_22,
inference(sat_conversion,[],[f596]) ).
cnf(s30,plain,
( ~ spl41_38
| spl41_39 ),
inference(sat_conversion,[],[f626]) ).
cnf(s33,plain,
( spl41_39
| ~ spl41_40 ),
inference(sat_conversion,[],[f642]) ).
cnf(s34,plain,
( ~ spl41_13
| spl41_39 ),
inference(sat_conversion,[],[f652]) ).
cnf(s38,plain,
( spl41_40
| spl41_43
| ~ spl41_44 ),
inference(sat_conversion,[],[f699]) ).
cnf(s62,plain,
( ~ spl41_21
| spl41_22 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s63,plain,
( ~ spl41_12
| spl41_40 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s64,plain,
( spl41_13
| ~ spl41_16 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s70,plain,
~ spl41_39,
inference(sat_conversion,[],[f1129]) ).
cnf(s88,plain,
( ~ spl41_11
| ~ spl41_14
| ~ spl41_15
| ~ spl41_20
| ~ spl41_23
| spl41_38
| spl41_44 ),
inference(sat_conversion,[],[f1271]) ).
cnf(s89,plain,
( ~ spl41_11
| ~ spl41_15
| ~ spl41_20
| ~ spl41_43 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s90,plain,
~ spl41_13,
inference(rat,[],[s34,s70]) ).
cnf(s91,plain,
~ spl41_16,
inference(rat,[],[s64,s90]) ).
cnf(s92,plain,
~ spl41_40,
inference(rat,[],[s33,s70]) ).
cnf(s93,plain,
~ spl41_12,
inference(rat,[],[s63,s92]) ).
cnf(s94,plain,
~ spl41_38,
inference(rat,[],[s30,s70]) ).
cnf(s95,plain,
~ spl41_21,
inference(rat,[],[s62,s23]) ).
cnf(s96,plain,
spl41_23,
inference(rat,[],[s15,s23]) ).
cnf(s97,plain,
spl41_20,
inference(rat,[],[s14,s95]) ).
cnf(s98,plain,
spl41_15,
inference(rat,[],[s9,s91]) ).
cnf(s99,plain,
spl41_14,
inference(rat,[],[s8,s90]) ).
cnf(s100,plain,
spl41_11,
inference(rat,[],[s7,s93]) ).
cnf(s101,plain,
~ spl41_43,
inference(rat,[],[s89,s98,s97,s100]) ).
cnf(s102,plain,
spl41_44,
inference(rat,[],[s88,s99,s94,s96,s97,s98,s100]) ).
cnf(s103,plain,
$false,
inference(rat,[],[s38,s92,s102,s101]) ).
fof(f1290,plain,
$false,
inference(avatar_sat_refutation,[],[s103]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV448+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.11/0.25 % Computer : n013.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.25 % DateTime : Mon Sep 28 11:08:06 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.31 Running first-order theorem proving
% 0.25/0.31 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
% 5.00/1.68 % (1103665)Detected formulas, will run a generic FOF schedule.
% 5.00/1.68 % (1103673)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4202902408:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.00/1.68 % (1103673)First to succeed.
% 5.00/1.68 % (1103673)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1103665"
% 5.00/1.68 % (1103675)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=565639997:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.00/1.68 % (1103676)dis-21_1_sil=8000:lcm=predicate:random_seed=922441572: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)
% 5.00/1.68 % (1103674)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2040694998:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.00/1.68 % (1103670)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=3904989519:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.00/1.68 % (1103672)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=4059932069:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.00/1.68 % (1103671)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=3050710609:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.00/1.68 % (1103674)Also succeeded, but the first one will report.
% 5.00/1.68 % (1103676)Instruction limit reached!
% 5.00/1.68 % (1103676)------------------------------
% 5.00/1.68 % (1103676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.68 % (1103676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.68 % (1103676)CaDiCaL version: 2.1.3
% 5.00/1.68 % (1103676)Termination reason: Instruction limit
% 5.00/1.68 % (1103676)Termination phase: Saturation
% 5.00/1.68 % (1103676)Time elapsed: 0.102 s
% 5.00/1.68 % (1103676)Peak memory usage: 89 MB
% 5.00/1.68 % (1103676)Instructions burned: 129 (million)
% 5.00/1.68 % (1103675)Also succeeded, but the first one will report.
% 5.00/1.68 % (1103684)lrs+10_1_sil=8000:sp=occurrence:random_seed=3277754501:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 5.00/1.68 % (1103673)Refutation found. Thanks to Tanya!
% 5.00/1.68 % SZS status Theorem for theBenchmark
% 5.00/1.68 % SZS output start Proof for theBenchmark
% See solution above
% 6.03/1.89 % (1103673)------------------------------
% 6.03/1.89 % (1103673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.03/1.89 % (1103673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.03/1.89 % (1103673)CaDiCaL version: 2.1.3
% 6.03/1.89 % (1103673)Termination reason: Refutation
% 6.03/1.89 % (1103673)Time elapsed: 0.026 s
% 6.03/1.89 % (1103673)Peak memory usage: 90 MB
% 6.03/1.89 % (1103673)Instructions burned: 44 (million)
% 6.03/1.89 % (1103673)------------------------------
% 6.03/1.89 % (1103673)------------------------------
% 6.03/1.89 % (1103665)Success in time 0.768 s
% 6.03/1.89 % Vampire exiting
%------------------------------------------------------------------------------