%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWV461+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Sun Dec 26 12:54:18 EST 2010
% Result : Theorem 10.31s
% Output : CNFRefutation 10.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 12
% Syntax : Number of formulae : 97 ( 38 unt; 0 def)
% Number of atoms : 1125 ( 465 equ)
% Maximal formula atoms : 115 ( 11 avg)
% Number of connectives : 1643 ( 615 ~; 469 |; 444 &)
% ( 5 <=>; 110 =>; 0 <=; 0 <~>)
% Maximal formula depth : 62 ( 8 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 4 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 19 con; 0-5 aty)
% Number of variables : 476 ( 9 sgn 431 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1,X2] :
( ( leq(X1,X2)
& leq(X2,X1) )
<=> X1 = X2 ),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',axiom_61) ).
fof(3,axiom,
! [X1,X2] : m_Down(X1) != m_Halt(X2),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',axiom_17) ).
fof(5,axiom,
! [X1,X2,X3] : m_Ack(X1,X2) != m_Halt(X3),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',axiom_11) ).
fof(19,axiom,
! [X5,X6] :
( elem(m_Ack(X5,X6),queue(host(X5)))
=> ( setIn(X5,pids)
& setIn(X6,pids) ) ),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',axiom) ).
fof(24,axiom,
! [X7] : leq(host(X7),nbr_proc),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',axiom_04) ).
fof(31,axiom,
! [X1,X2,X4] :
( elem(X1,snoc(X4,X2))
<=> ( X1 = X2
| elem(X1,X4) ) ),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',axiom_47) ).
fof(38,axiom,
! [X1] : leq(X1,X1),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',axiom_59) ).
fof(44,conjecture,
! [X12,X13] :
( ( ! [X1] :
( host(X13) = host(X1)
=> ~ setIn(X1,alive) )
& ! [X1,X2] :
( elem(m_Ldr(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2] :
( elem(m_Down(X2),queue(host(X1)))
=> host(X2) != host(X1) )
& ! [X1,X2] :
( elem(m_Halt(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2,X3] :
( elem(m_Ack(X3,X1),queue(host(X2)))
=> ~ leq(host(X1),host(X3)) )
& ! [X1,X2] :
( ( X2 != X1
& host(X2) = host(X1) )
=> ( ~ setIn(X1,alive)
| ~ setIn(X2,alive) ) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& elem(m_Ack(X2,X1),queue(host(X2))) )
=> leq(host(X1),index(pendack,host(X2))) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& index(status,host(X2)) = elec_1 )
=> ~ elem(m_Ack(X2,X1),queue(host(X2))) )
& ! [X1] :
( ( ( index(status,host(X1)) = elec_1
| index(status,host(X1)) = elec_2 )
& setIn(X1,alive) )
=> index(elid,host(X1)) = X1 )
& ! [X1,X2,X3] :
( ( setIn(X3,alive)
& elem(m_Down(X2),queue(host(X3)))
& host(X2) = host(X1) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3] :
( ( setIn(X1,alive)
& setIn(X3,alive)
& host(X3) = host(X2)
& index(status,host(X1)) = elec_2
& index(status,host(X3)) = elec_2 )
=> ~ elem(m_Ack(X1,X2),queue(host(X1))) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> leq(index(pendack,host(X2)),host(X1)) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> ~ leq(index(pendack,host(X1)),index(pendack,host(X2))) )
& ! [X1,X2,X3] :
( ( ~ leq(index(pendack,host(X3)),host(X1))
& setIn(X3,alive)
& elem(m_Halt(X3),queue(host(X2)))
& index(status,host(X3)) = elec_2 )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3,X14] :
( ( ! [X15] :
( ( ~ leq(host(X14),X15)
& leq(s(zero),X15) )
=> ( setIn(X15,index(down,host(X14)))
| X15 = host(X3) ) )
& elem(m_Down(X3),queue(host(X14)))
& host(X14) = host(X2)
& host(X14) = nbr_proc
& index(status,host(X14)) = elec_1 )
=> ~ ( setIn(X1,alive)
& elem(m_Down(X2),queue(host(X1))) ) )
& ! [X1,X2,X3,X14] :
( ( setIn(X14,alive)
& elem(m_Down(X3),queue(host(X14)))
& elem(m_Ack(X14,X2),queue(host(X14)))
& leq(nbr_proc,s(index(pendack,host(X14))))
& index(status,host(X14)) = elec_2
& host(X2) = index(pendack,host(X14))
& host(X3) = s(index(pendack,host(X14))) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) )
=> ( queue(host(X13)) = q_nil
=> ( ( ! [X1] :
( host(X13) = host(X1)
=> leq(X1,X12) )
& ~ setIn(X12,pids)
& host(X13) = host(X12) )
=> ( host(X12) = s(zero)
=> ( ~ leq(nbr_proc,host(X12))
=> ! [X1] :
( host(X12) != host(X1)
=> ! [X2,X3,X16] :
( s(host(X12)) = host(X16)
=> ( host(X12) != host(X16)
=> ( ( ( setIn(X16,alive)
| X16 = X12 )
& leq(nbr_proc,s(index(pendack,host(X16))))
& elem(m_Down(X3),snoc(queue(host(X16)),m_Halt(X12)))
& elem(m_Ack(X16,X2),snoc(queue(host(X16)),m_Halt(X12)))
& index(status,host(X16)) = elec_2
& host(X2) = index(pendack,host(X16))
& host(X3) = s(index(pendack,host(X16))) )
=> ~ ( ( setIn(X1,alive)
| X1 = X12 )
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) ) ) ) ) ) ) ) ),
file('/tmp/tmpEAAMfW/sel_SWV461+1.p_1',conj) ).
fof(45,negated_conjecture,
~ ! [X12,X13] :
( ( ! [X1] :
( host(X13) = host(X1)
=> ~ setIn(X1,alive) )
& ! [X1,X2] :
( elem(m_Ldr(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2] :
( elem(m_Down(X2),queue(host(X1)))
=> host(X2) != host(X1) )
& ! [X1,X2] :
( elem(m_Halt(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2,X3] :
( elem(m_Ack(X3,X1),queue(host(X2)))
=> ~ leq(host(X1),host(X3)) )
& ! [X1,X2] :
( ( X2 != X1
& host(X2) = host(X1) )
=> ( ~ setIn(X1,alive)
| ~ setIn(X2,alive) ) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& elem(m_Ack(X2,X1),queue(host(X2))) )
=> leq(host(X1),index(pendack,host(X2))) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& index(status,host(X2)) = elec_1 )
=> ~ elem(m_Ack(X2,X1),queue(host(X2))) )
& ! [X1] :
( ( ( index(status,host(X1)) = elec_1
| index(status,host(X1)) = elec_2 )
& setIn(X1,alive) )
=> index(elid,host(X1)) = X1 )
& ! [X1,X2,X3] :
( ( setIn(X3,alive)
& elem(m_Down(X2),queue(host(X3)))
& host(X2) = host(X1) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3] :
( ( setIn(X1,alive)
& setIn(X3,alive)
& host(X3) = host(X2)
& index(status,host(X1)) = elec_2
& index(status,host(X3)) = elec_2 )
=> ~ elem(m_Ack(X1,X2),queue(host(X1))) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> leq(index(pendack,host(X2)),host(X1)) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> ~ leq(index(pendack,host(X1)),index(pendack,host(X2))) )
& ! [X1,X2,X3] :
( ( ~ leq(index(pendack,host(X3)),host(X1))
& setIn(X3,alive)
& elem(m_Halt(X3),queue(host(X2)))
& index(status,host(X3)) = elec_2 )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3,X14] :
( ( ! [X15] :
( ( ~ leq(host(X14),X15)
& leq(s(zero),X15) )
=> ( setIn(X15,index(down,host(X14)))
| X15 = host(X3) ) )
& elem(m_Down(X3),queue(host(X14)))
& host(X14) = host(X2)
& host(X14) = nbr_proc
& index(status,host(X14)) = elec_1 )
=> ~ ( setIn(X1,alive)
& elem(m_Down(X2),queue(host(X1))) ) )
& ! [X1,X2,X3,X14] :
( ( setIn(X14,alive)
& elem(m_Down(X3),queue(host(X14)))
& elem(m_Ack(X14,X2),queue(host(X14)))
& leq(nbr_proc,s(index(pendack,host(X14))))
& index(status,host(X14)) = elec_2
& host(X2) = index(pendack,host(X14))
& host(X3) = s(index(pendack,host(X14))) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) )
=> ( queue(host(X13)) = q_nil
=> ( ( ! [X1] :
( host(X13) = host(X1)
=> leq(X1,X12) )
& ~ setIn(X12,pids)
& host(X13) = host(X12) )
=> ( host(X12) = s(zero)
=> ( ~ leq(nbr_proc,host(X12))
=> ! [X1] :
( host(X12) != host(X1)
=> ! [X2,X3,X16] :
( s(host(X12)) = host(X16)
=> ( host(X12) != host(X16)
=> ( ( ( setIn(X16,alive)
| X16 = X12 )
& leq(nbr_proc,s(index(pendack,host(X16))))
& elem(m_Down(X3),snoc(queue(host(X16)),m_Halt(X12)))
& elem(m_Ack(X16,X2),snoc(queue(host(X16)),m_Halt(X12)))
& index(status,host(X16)) = elec_2
& host(X2) = index(pendack,host(X16))
& host(X3) = s(index(pendack,host(X16))) )
=> ~ ( ( setIn(X1,alive)
| X1 = X12 )
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) ) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[44]) ).
fof(49,negated_conjecture,
~ ! [X12,X13] :
( ( ! [X1] :
( host(X13) = host(X1)
=> ~ setIn(X1,alive) )
& ! [X1,X2] :
( elem(m_Ldr(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2] :
( elem(m_Down(X2),queue(host(X1)))
=> host(X2) != host(X1) )
& ! [X1,X2] :
( elem(m_Halt(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2,X3] :
( elem(m_Ack(X3,X1),queue(host(X2)))
=> ~ leq(host(X1),host(X3)) )
& ! [X1,X2] :
( ( X2 != X1
& host(X2) = host(X1) )
=> ( ~ setIn(X1,alive)
| ~ setIn(X2,alive) ) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& elem(m_Ack(X2,X1),queue(host(X2))) )
=> leq(host(X1),index(pendack,host(X2))) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& index(status,host(X2)) = elec_1 )
=> ~ elem(m_Ack(X2,X1),queue(host(X2))) )
& ! [X1] :
( ( ( index(status,host(X1)) = elec_1
| index(status,host(X1)) = elec_2 )
& setIn(X1,alive) )
=> index(elid,host(X1)) = X1 )
& ! [X1,X2,X3] :
( ( setIn(X3,alive)
& elem(m_Down(X2),queue(host(X3)))
& host(X2) = host(X1) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3] :
( ( setIn(X1,alive)
& setIn(X3,alive)
& host(X3) = host(X2)
& index(status,host(X1)) = elec_2
& index(status,host(X3)) = elec_2 )
=> ~ elem(m_Ack(X1,X2),queue(host(X1))) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> leq(index(pendack,host(X2)),host(X1)) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> ~ leq(index(pendack,host(X1)),index(pendack,host(X2))) )
& ! [X1,X2,X3] :
( ( ~ leq(index(pendack,host(X3)),host(X1))
& setIn(X3,alive)
& elem(m_Halt(X3),queue(host(X2)))
& index(status,host(X3)) = elec_2 )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3,X14] :
( ( ! [X15] :
( ( ~ leq(host(X14),X15)
& leq(s(zero),X15) )
=> ( setIn(X15,index(down,host(X14)))
| X15 = host(X3) ) )
& elem(m_Down(X3),queue(host(X14)))
& host(X14) = host(X2)
& host(X14) = nbr_proc
& index(status,host(X14)) = elec_1 )
=> ~ ( setIn(X1,alive)
& elem(m_Down(X2),queue(host(X1))) ) )
& ! [X1,X2,X3,X14] :
( ( setIn(X14,alive)
& elem(m_Down(X3),queue(host(X14)))
& elem(m_Ack(X14,X2),queue(host(X14)))
& leq(nbr_proc,s(index(pendack,host(X14))))
& index(status,host(X14)) = elec_2
& host(X2) = index(pendack,host(X14))
& host(X3) = s(index(pendack,host(X14))) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) )
=> ( queue(host(X13)) = q_nil
=> ( ( ! [X1] :
( host(X13) = host(X1)
=> leq(X1,X12) )
& ~ setIn(X12,pids)
& host(X13) = host(X12) )
=> ( host(X12) = s(zero)
=> ( ~ leq(nbr_proc,host(X12))
=> ! [X1] :
( host(X12) != host(X1)
=> ! [X2,X3,X16] :
( s(host(X12)) = host(X16)
=> ( host(X12) != host(X16)
=> ( ( ( setIn(X16,alive)
| X16 = X12 )
& leq(nbr_proc,s(index(pendack,host(X16))))
& elem(m_Down(X3),snoc(queue(host(X16)),m_Halt(X12)))
& elem(m_Ack(X16,X2),snoc(queue(host(X16)),m_Halt(X12)))
& index(status,host(X16)) = elec_2
& host(X2) = index(pendack,host(X16))
& host(X3) = s(index(pendack,host(X16))) )
=> ~ ( ( setIn(X1,alive)
| X1 = X12 )
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[45,theory(equality)]) ).
fof(50,plain,
! [X13] :
( epred1_1(X13)
=> ( ! [X1] :
( host(X13) = host(X1)
=> ~ setIn(X1,alive) )
& ! [X1,X2] :
( elem(m_Ldr(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2] :
( elem(m_Down(X2),queue(host(X1)))
=> host(X2) != host(X1) )
& ! [X1,X2] :
( elem(m_Halt(X2),queue(host(X1)))
=> ~ leq(host(X1),host(X2)) )
& ! [X1,X2,X3] :
( elem(m_Ack(X3,X1),queue(host(X2)))
=> ~ leq(host(X1),host(X3)) )
& ! [X1,X2] :
( ( X2 != X1
& host(X2) = host(X1) )
=> ( ~ setIn(X1,alive)
| ~ setIn(X2,alive) ) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& elem(m_Ack(X2,X1),queue(host(X2))) )
=> leq(host(X1),index(pendack,host(X2))) )
& ! [X1,X2] :
( ( setIn(X2,alive)
& index(status,host(X2)) = elec_1 )
=> ~ elem(m_Ack(X2,X1),queue(host(X2))) )
& ! [X1] :
( ( ( index(status,host(X1)) = elec_1
| index(status,host(X1)) = elec_2 )
& setIn(X1,alive) )
=> index(elid,host(X1)) = X1 )
& ! [X1,X2,X3] :
( ( setIn(X3,alive)
& elem(m_Down(X2),queue(host(X3)))
& host(X2) = host(X1) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3] :
( ( setIn(X1,alive)
& setIn(X3,alive)
& host(X3) = host(X2)
& index(status,host(X1)) = elec_2
& index(status,host(X3)) = elec_2 )
=> ~ elem(m_Ack(X1,X2),queue(host(X1))) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> leq(index(pendack,host(X2)),host(X1)) )
& ! [X1,X2] :
( ( ~ leq(host(X1),host(X2))
& setIn(X1,alive)
& setIn(X2,alive)
& index(status,host(X1)) = elec_2
& index(status,host(X2)) = elec_2 )
=> ~ leq(index(pendack,host(X1)),index(pendack,host(X2))) )
& ! [X1,X2,X3] :
( ( ~ leq(index(pendack,host(X3)),host(X1))
& setIn(X3,alive)
& elem(m_Halt(X3),queue(host(X2)))
& index(status,host(X3)) = elec_2 )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) )
& ! [X1,X2,X3,X14] :
( ( ! [X15] :
( ( ~ leq(host(X14),X15)
& leq(s(zero),X15) )
=> ( setIn(X15,index(down,host(X14)))
| X15 = host(X3) ) )
& elem(m_Down(X3),queue(host(X14)))
& host(X14) = host(X2)
& host(X14) = nbr_proc
& index(status,host(X14)) = elec_1 )
=> ~ ( setIn(X1,alive)
& elem(m_Down(X2),queue(host(X1))) ) )
& ! [X1,X2,X3,X14] :
( ( setIn(X14,alive)
& elem(m_Down(X3),queue(host(X14)))
& elem(m_Ack(X14,X2),queue(host(X14)))
& leq(nbr_proc,s(index(pendack,host(X14))))
& index(status,host(X14)) = elec_2
& host(X2) = index(pendack,host(X14))
& host(X3) = s(index(pendack,host(X14))) )
=> ~ ( setIn(X1,alive)
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) ) ),
introduced(definition) ).
fof(51,negated_conjecture,
~ ! [X12,X13] :
( epred1_1(X13)
=> ( queue(host(X13)) = q_nil
=> ( ( ! [X1] :
( host(X13) = host(X1)
=> leq(X1,X12) )
& ~ setIn(X12,pids)
& host(X13) = host(X12) )
=> ( host(X12) = s(zero)
=> ( ~ leq(nbr_proc,host(X12))
=> ! [X1] :
( host(X12) != host(X1)
=> ! [X2,X3,X16] :
( s(host(X12)) = host(X16)
=> ( host(X12) != host(X16)
=> ( ( ( setIn(X16,alive)
| X16 = X12 )
& leq(nbr_proc,s(index(pendack,host(X16))))
& elem(m_Down(X3),snoc(queue(host(X16)),m_Halt(X12)))
& elem(m_Ack(X16,X2),snoc(queue(host(X16)),m_Halt(X12)))
& index(status,host(X16)) = elec_2
& host(X2) = index(pendack,host(X16))
& host(X3) = s(index(pendack,host(X16))) )
=> ~ ( ( setIn(X1,alive)
| X1 = X12 )
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) ) ) ) ) ) ) ) ),
inference(apply_def,[status(esa)],[49,50,theory(equality)]) ).
fof(54,plain,
! [X1,X2] :
( ( ~ leq(X1,X2)
| ~ leq(X2,X1)
| X1 = X2 )
& ( X1 != X2
| ( leq(X1,X2)
& leq(X2,X1) ) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(55,plain,
! [X3,X4] :
( ( ~ leq(X3,X4)
| ~ leq(X4,X3)
| X3 = X4 )
& ( X3 != X4
| ( leq(X3,X4)
& leq(X4,X3) ) ) ),
inference(variable_rename,[status(thm)],[54]) ).
fof(56,plain,
! [X3,X4] :
( ( ~ leq(X3,X4)
| ~ leq(X4,X3)
| X3 = X4 )
& ( leq(X3,X4)
| X3 != X4 )
& ( leq(X4,X3)
| X3 != X4 ) ),
inference(distribute,[status(thm)],[55]) ).
cnf(59,plain,
( X1 = X2
| ~ leq(X2,X1)
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[56]) ).
fof(60,plain,
! [X3,X4] : m_Down(X3) != m_Halt(X4),
inference(variable_rename,[status(thm)],[3]) ).
cnf(61,plain,
m_Down(X1) != m_Halt(X2),
inference(split_conjunct,[status(thm)],[60]) ).
fof(63,plain,
! [X4,X5,X6] : m_Ack(X4,X5) != m_Halt(X6),
inference(variable_rename,[status(thm)],[5]) ).
cnf(64,plain,
m_Ack(X1,X2) != m_Halt(X3),
inference(split_conjunct,[status(thm)],[63]) ).
fof(105,plain,
! [X5,X6] :
( ~ elem(m_Ack(X5,X6),queue(host(X5)))
| ( setIn(X5,pids)
& setIn(X6,pids) ) ),
inference(fof_nnf,[status(thm)],[19]) ).
fof(106,plain,
! [X7,X8] :
( ~ elem(m_Ack(X7,X8),queue(host(X7)))
| ( setIn(X7,pids)
& setIn(X8,pids) ) ),
inference(variable_rename,[status(thm)],[105]) ).
fof(107,plain,
! [X7,X8] :
( ( setIn(X7,pids)
| ~ elem(m_Ack(X7,X8),queue(host(X7))) )
& ( setIn(X8,pids)
| ~ elem(m_Ack(X7,X8),queue(host(X7))) ) ),
inference(distribute,[status(thm)],[106]) ).
cnf(109,plain,
( setIn(X1,pids)
| ~ elem(m_Ack(X1,X2),queue(host(X1))) ),
inference(split_conjunct,[status(thm)],[107]) ).
fof(115,plain,
! [X8] : leq(host(X8),nbr_proc),
inference(variable_rename,[status(thm)],[24]) ).
cnf(116,plain,
leq(host(X1),nbr_proc),
inference(split_conjunct,[status(thm)],[115]) ).
fof(129,plain,
! [X1,X2,X4] :
( ( ~ elem(X1,snoc(X4,X2))
| X1 = X2
| elem(X1,X4) )
& ( ( X1 != X2
& ~ elem(X1,X4) )
| elem(X1,snoc(X4,X2)) ) ),
inference(fof_nnf,[status(thm)],[31]) ).
fof(130,plain,
! [X5,X6,X7] :
( ( ~ elem(X5,snoc(X7,X6))
| X5 = X6
| elem(X5,X7) )
& ( ( X5 != X6
& ~ elem(X5,X7) )
| elem(X5,snoc(X7,X6)) ) ),
inference(variable_rename,[status(thm)],[129]) ).
fof(131,plain,
! [X5,X6,X7] :
( ( ~ elem(X5,snoc(X7,X6))
| X5 = X6
| elem(X5,X7) )
& ( X5 != X6
| elem(X5,snoc(X7,X6)) )
& ( ~ elem(X5,X7)
| elem(X5,snoc(X7,X6)) ) ),
inference(distribute,[status(thm)],[130]) ).
cnf(134,plain,
( elem(X1,X2)
| X1 = X3
| ~ elem(X1,snoc(X2,X3)) ),
inference(split_conjunct,[status(thm)],[131]) ).
fof(149,plain,
! [X2] : leq(X2,X2),
inference(variable_rename,[status(thm)],[38]) ).
cnf(150,plain,
leq(X1,X1),
inference(split_conjunct,[status(thm)],[149]) ).
fof(165,negated_conjecture,
? [X12,X13] :
( epred1_1(X13)
& queue(host(X13)) = q_nil
& ! [X1] :
( host(X13) != host(X1)
| leq(X1,X12) )
& ~ setIn(X12,pids)
& host(X13) = host(X12)
& host(X12) = s(zero)
& ~ leq(nbr_proc,host(X12))
& ? [X1] :
( host(X12) != host(X1)
& ? [X2,X3,X16] :
( s(host(X12)) = host(X16)
& host(X12) != host(X16)
& ( setIn(X16,alive)
| X16 = X12 )
& leq(nbr_proc,s(index(pendack,host(X16))))
& elem(m_Down(X3),snoc(queue(host(X16)),m_Halt(X12)))
& elem(m_Ack(X16,X2),snoc(queue(host(X16)),m_Halt(X12)))
& index(status,host(X16)) = elec_2
& host(X2) = index(pendack,host(X16))
& host(X3) = s(index(pendack,host(X16)))
& ( setIn(X1,alive)
| X1 = X12 )
& index(ldr,host(X1)) = host(X1)
& index(status,host(X1)) = norm ) ) ),
inference(fof_nnf,[status(thm)],[51]) ).
fof(166,negated_conjecture,
? [X17,X18] :
( epred1_1(X18)
& queue(host(X18)) = q_nil
& ! [X19] :
( host(X18) != host(X19)
| leq(X19,X17) )
& ~ setIn(X17,pids)
& host(X18) = host(X17)
& host(X17) = s(zero)
& ~ leq(nbr_proc,host(X17))
& ? [X20] :
( host(X17) != host(X20)
& ? [X21,X22,X23] :
( s(host(X17)) = host(X23)
& host(X17) != host(X23)
& ( setIn(X23,alive)
| X23 = X17 )
& leq(nbr_proc,s(index(pendack,host(X23))))
& elem(m_Down(X22),snoc(queue(host(X23)),m_Halt(X17)))
& elem(m_Ack(X23,X21),snoc(queue(host(X23)),m_Halt(X17)))
& index(status,host(X23)) = elec_2
& host(X21) = index(pendack,host(X23))
& host(X22) = s(index(pendack,host(X23)))
& ( setIn(X20,alive)
| X20 = X17 )
& index(ldr,host(X20)) = host(X20)
& index(status,host(X20)) = norm ) ) ),
inference(variable_rename,[status(thm)],[165]) ).
fof(167,negated_conjecture,
( epred1_1(esk2_0)
& queue(host(esk2_0)) = q_nil
& ! [X19] :
( host(esk2_0) != host(X19)
| leq(X19,esk1_0) )
& ~ setIn(esk1_0,pids)
& host(esk2_0) = host(esk1_0)
& host(esk1_0) = s(zero)
& ~ leq(nbr_proc,host(esk1_0))
& host(esk1_0) != host(esk3_0)
& s(host(esk1_0)) = host(esk6_0)
& host(esk1_0) != host(esk6_0)
& ( setIn(esk6_0,alive)
| esk6_0 = esk1_0 )
& leq(nbr_proc,s(index(pendack,host(esk6_0))))
& elem(m_Down(esk5_0),snoc(queue(host(esk6_0)),m_Halt(esk1_0)))
& elem(m_Ack(esk6_0,esk4_0),snoc(queue(host(esk6_0)),m_Halt(esk1_0)))
& index(status,host(esk6_0)) = elec_2
& host(esk4_0) = index(pendack,host(esk6_0))
& host(esk5_0) = s(index(pendack,host(esk6_0)))
& ( setIn(esk3_0,alive)
| esk3_0 = esk1_0 )
& index(ldr,host(esk3_0)) = host(esk3_0)
& index(status,host(esk3_0)) = norm ),
inference(skolemize,[status(esa)],[166]) ).
fof(168,negated_conjecture,
! [X19] :
( ( host(esk2_0) != host(X19)
| leq(X19,esk1_0) )
& ~ setIn(esk1_0,pids)
& host(esk2_0) = host(esk1_0)
& host(esk1_0) = s(zero)
& ~ leq(nbr_proc,host(esk1_0))
& host(esk1_0) != host(esk3_0)
& s(host(esk1_0)) = host(esk6_0)
& host(esk1_0) != host(esk6_0)
& ( setIn(esk6_0,alive)
| esk6_0 = esk1_0 )
& leq(nbr_proc,s(index(pendack,host(esk6_0))))
& elem(m_Down(esk5_0),snoc(queue(host(esk6_0)),m_Halt(esk1_0)))
& elem(m_Ack(esk6_0,esk4_0),snoc(queue(host(esk6_0)),m_Halt(esk1_0)))
& index(status,host(esk6_0)) = elec_2
& host(esk4_0) = index(pendack,host(esk6_0))
& host(esk5_0) = s(index(pendack,host(esk6_0)))
& ( setIn(esk3_0,alive)
| esk3_0 = esk1_0 )
& index(ldr,host(esk3_0)) = host(esk3_0)
& index(status,host(esk3_0)) = norm
& queue(host(esk2_0)) = q_nil
& epred1_1(esk2_0) ),
inference(shift_quantors,[status(thm)],[167]) ).
cnf(169,negated_conjecture,
epred1_1(esk2_0),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(171,negated_conjecture,
index(status,host(esk3_0)) = norm,
inference(split_conjunct,[status(thm)],[168]) ).
cnf(172,negated_conjecture,
index(ldr,host(esk3_0)) = host(esk3_0),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(173,negated_conjecture,
( esk3_0 = esk1_0
| setIn(esk3_0,alive) ),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(174,negated_conjecture,
host(esk5_0) = s(index(pendack,host(esk6_0))),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(175,negated_conjecture,
host(esk4_0) = index(pendack,host(esk6_0)),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(176,negated_conjecture,
index(status,host(esk6_0)) = elec_2,
inference(split_conjunct,[status(thm)],[168]) ).
cnf(177,negated_conjecture,
elem(m_Ack(esk6_0,esk4_0),snoc(queue(host(esk6_0)),m_Halt(esk1_0))),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(178,negated_conjecture,
elem(m_Down(esk5_0),snoc(queue(host(esk6_0)),m_Halt(esk1_0))),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(179,negated_conjecture,
leq(nbr_proc,s(index(pendack,host(esk6_0)))),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(180,negated_conjecture,
( esk6_0 = esk1_0
| setIn(esk6_0,alive) ),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(183,negated_conjecture,
host(esk1_0) != host(esk3_0),
inference(split_conjunct,[status(thm)],[168]) ).
cnf(187,negated_conjecture,
~ setIn(esk1_0,pids),
inference(split_conjunct,[status(thm)],[168]) ).
fof(189,plain,
! [X13] :
( ~ epred1_1(X13)
| ( ! [X1] :
( host(X13) != host(X1)
| ~ setIn(X1,alive) )
& ! [X1,X2] :
( ~ elem(m_Ldr(X2),queue(host(X1)))
| ~ leq(host(X1),host(X2)) )
& ! [X1,X2] :
( ~ elem(m_Down(X2),queue(host(X1)))
| host(X2) != host(X1) )
& ! [X1,X2] :
( ~ elem(m_Halt(X2),queue(host(X1)))
| ~ leq(host(X1),host(X2)) )
& ! [X1,X2,X3] :
( ~ elem(m_Ack(X3,X1),queue(host(X2)))
| ~ leq(host(X1),host(X3)) )
& ! [X1,X2] :
( X2 = X1
| host(X2) != host(X1)
| ~ setIn(X1,alive)
| ~ setIn(X2,alive) )
& ! [X1,X2] :
( ~ setIn(X2,alive)
| ~ elem(m_Ack(X2,X1),queue(host(X2)))
| leq(host(X1),index(pendack,host(X2))) )
& ! [X1,X2] :
( ~ setIn(X2,alive)
| index(status,host(X2)) != elec_1
| ~ elem(m_Ack(X2,X1),queue(host(X2))) )
& ! [X1] :
( ( index(status,host(X1)) != elec_1
& index(status,host(X1)) != elec_2 )
| ~ setIn(X1,alive)
| index(elid,host(X1)) = X1 )
& ! [X1,X2,X3] :
( ~ setIn(X3,alive)
| ~ elem(m_Down(X2),queue(host(X3)))
| host(X2) != host(X1)
| ~ setIn(X1,alive)
| index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm )
& ! [X1,X2,X3] :
( ~ setIn(X1,alive)
| ~ setIn(X3,alive)
| host(X3) != host(X2)
| index(status,host(X1)) != elec_2
| index(status,host(X3)) != elec_2
| ~ elem(m_Ack(X1,X2),queue(host(X1))) )
& ! [X1,X2] :
( leq(host(X1),host(X2))
| ~ setIn(X1,alive)
| ~ setIn(X2,alive)
| index(status,host(X1)) != elec_2
| index(status,host(X2)) != elec_2
| leq(index(pendack,host(X2)),host(X1)) )
& ! [X1,X2] :
( leq(host(X1),host(X2))
| ~ setIn(X1,alive)
| ~ setIn(X2,alive)
| index(status,host(X1)) != elec_2
| index(status,host(X2)) != elec_2
| ~ leq(index(pendack,host(X1)),index(pendack,host(X2))) )
& ! [X1,X2,X3] :
( leq(index(pendack,host(X3)),host(X1))
| ~ setIn(X3,alive)
| ~ elem(m_Halt(X3),queue(host(X2)))
| index(status,host(X3)) != elec_2
| ~ setIn(X1,alive)
| index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm )
& ! [X1,X2,X3,X14] :
( ? [X15] :
( ~ leq(host(X14),X15)
& leq(s(zero),X15)
& ~ setIn(X15,index(down,host(X14)))
& X15 != host(X3) )
| ~ elem(m_Down(X3),queue(host(X14)))
| host(X14) != host(X2)
| host(X14) != nbr_proc
| index(status,host(X14)) != elec_1
| ~ setIn(X1,alive)
| ~ elem(m_Down(X2),queue(host(X1))) )
& ! [X1,X2,X3,X14] :
( ~ setIn(X14,alive)
| ~ elem(m_Down(X3),queue(host(X14)))
| ~ elem(m_Ack(X14,X2),queue(host(X14)))
| ~ leq(nbr_proc,s(index(pendack,host(X14))))
| index(status,host(X14)) != elec_2
| host(X2) != index(pendack,host(X14))
| host(X3) != s(index(pendack,host(X14)))
| ~ setIn(X1,alive)
| index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm ) ) ),
inference(fof_nnf,[status(thm)],[50]) ).
fof(190,plain,
! [X16] :
( ~ epred1_1(X16)
| ( ! [X17] :
( host(X16) != host(X17)
| ~ setIn(X17,alive) )
& ! [X18,X19] :
( ~ elem(m_Ldr(X19),queue(host(X18)))
| ~ leq(host(X18),host(X19)) )
& ! [X20,X21] :
( ~ elem(m_Down(X21),queue(host(X20)))
| host(X21) != host(X20) )
& ! [X22,X23] :
( ~ elem(m_Halt(X23),queue(host(X22)))
| ~ leq(host(X22),host(X23)) )
& ! [X24,X25,X26] :
( ~ elem(m_Ack(X26,X24),queue(host(X25)))
| ~ leq(host(X24),host(X26)) )
& ! [X27,X28] :
( X28 = X27
| host(X28) != host(X27)
| ~ setIn(X27,alive)
| ~ setIn(X28,alive) )
& ! [X29,X30] :
( ~ setIn(X30,alive)
| ~ elem(m_Ack(X30,X29),queue(host(X30)))
| leq(host(X29),index(pendack,host(X30))) )
& ! [X31,X32] :
( ~ setIn(X32,alive)
| index(status,host(X32)) != elec_1
| ~ elem(m_Ack(X32,X31),queue(host(X32))) )
& ! [X33] :
( ( index(status,host(X33)) != elec_1
& index(status,host(X33)) != elec_2 )
| ~ setIn(X33,alive)
| index(elid,host(X33)) = X33 )
& ! [X34,X35,X36] :
( ~ setIn(X36,alive)
| ~ elem(m_Down(X35),queue(host(X36)))
| host(X35) != host(X34)
| ~ setIn(X34,alive)
| index(ldr,host(X34)) != host(X34)
| index(status,host(X34)) != norm )
& ! [X37,X38,X39] :
( ~ setIn(X37,alive)
| ~ setIn(X39,alive)
| host(X39) != host(X38)
| index(status,host(X37)) != elec_2
| index(status,host(X39)) != elec_2
| ~ elem(m_Ack(X37,X38),queue(host(X37))) )
& ! [X40,X41] :
( leq(host(X40),host(X41))
| ~ setIn(X40,alive)
| ~ setIn(X41,alive)
| index(status,host(X40)) != elec_2
| index(status,host(X41)) != elec_2
| leq(index(pendack,host(X41)),host(X40)) )
& ! [X42,X43] :
( leq(host(X42),host(X43))
| ~ setIn(X42,alive)
| ~ setIn(X43,alive)
| index(status,host(X42)) != elec_2
| index(status,host(X43)) != elec_2
| ~ leq(index(pendack,host(X42)),index(pendack,host(X43))) )
& ! [X44,X45,X46] :
( leq(index(pendack,host(X46)),host(X44))
| ~ setIn(X46,alive)
| ~ elem(m_Halt(X46),queue(host(X45)))
| index(status,host(X46)) != elec_2
| ~ setIn(X44,alive)
| index(ldr,host(X44)) != host(X44)
| index(status,host(X44)) != norm )
& ! [X47,X48,X49,X50] :
( ? [X51] :
( ~ leq(host(X50),X51)
& leq(s(zero),X51)
& ~ setIn(X51,index(down,host(X50)))
& X51 != host(X49) )
| ~ elem(m_Down(X49),queue(host(X50)))
| host(X50) != host(X48)
| host(X50) != nbr_proc
| index(status,host(X50)) != elec_1
| ~ setIn(X47,alive)
| ~ elem(m_Down(X48),queue(host(X47))) )
& ! [X52,X53,X54,X55] :
( ~ setIn(X55,alive)
| ~ elem(m_Down(X54),queue(host(X55)))
| ~ elem(m_Ack(X55,X53),queue(host(X55)))
| ~ leq(nbr_proc,s(index(pendack,host(X55))))
| index(status,host(X55)) != elec_2
| host(X53) != index(pendack,host(X55))
| host(X54) != s(index(pendack,host(X55)))
| ~ setIn(X52,alive)
| index(ldr,host(X52)) != host(X52)
| index(status,host(X52)) != norm ) ) ),
inference(variable_rename,[status(thm)],[189]) ).
fof(191,plain,
! [X16] :
( ~ epred1_1(X16)
| ( ! [X17] :
( host(X16) != host(X17)
| ~ setIn(X17,alive) )
& ! [X18,X19] :
( ~ elem(m_Ldr(X19),queue(host(X18)))
| ~ leq(host(X18),host(X19)) )
& ! [X20,X21] :
( ~ elem(m_Down(X21),queue(host(X20)))
| host(X21) != host(X20) )
& ! [X22,X23] :
( ~ elem(m_Halt(X23),queue(host(X22)))
| ~ leq(host(X22),host(X23)) )
& ! [X24,X25,X26] :
( ~ elem(m_Ack(X26,X24),queue(host(X25)))
| ~ leq(host(X24),host(X26)) )
& ! [X27,X28] :
( X28 = X27
| host(X28) != host(X27)
| ~ setIn(X27,alive)
| ~ setIn(X28,alive) )
& ! [X29,X30] :
( ~ setIn(X30,alive)
| ~ elem(m_Ack(X30,X29),queue(host(X30)))
| leq(host(X29),index(pendack,host(X30))) )
& ! [X31,X32] :
( ~ setIn(X32,alive)
| index(status,host(X32)) != elec_1
| ~ elem(m_Ack(X32,X31),queue(host(X32))) )
& ! [X33] :
( ( index(status,host(X33)) != elec_1
& index(status,host(X33)) != elec_2 )
| ~ setIn(X33,alive)
| index(elid,host(X33)) = X33 )
& ! [X34,X35,X36] :
( ~ setIn(X36,alive)
| ~ elem(m_Down(X35),queue(host(X36)))
| host(X35) != host(X34)
| ~ setIn(X34,alive)
| index(ldr,host(X34)) != host(X34)
| index(status,host(X34)) != norm )
& ! [X37,X38,X39] :
( ~ setIn(X37,alive)
| ~ setIn(X39,alive)
| host(X39) != host(X38)
| index(status,host(X37)) != elec_2
| index(status,host(X39)) != elec_2
| ~ elem(m_Ack(X37,X38),queue(host(X37))) )
& ! [X40,X41] :
( leq(host(X40),host(X41))
| ~ setIn(X40,alive)
| ~ setIn(X41,alive)
| index(status,host(X40)) != elec_2
| index(status,host(X41)) != elec_2
| leq(index(pendack,host(X41)),host(X40)) )
& ! [X42,X43] :
( leq(host(X42),host(X43))
| ~ setIn(X42,alive)
| ~ setIn(X43,alive)
| index(status,host(X42)) != elec_2
| index(status,host(X43)) != elec_2
| ~ leq(index(pendack,host(X42)),index(pendack,host(X43))) )
& ! [X44,X45,X46] :
( leq(index(pendack,host(X46)),host(X44))
| ~ setIn(X46,alive)
| ~ elem(m_Halt(X46),queue(host(X45)))
| index(status,host(X46)) != elec_2
| ~ setIn(X44,alive)
| index(ldr,host(X44)) != host(X44)
| index(status,host(X44)) != norm )
& ! [X47,X48,X49,X50] :
( ( ~ leq(host(X50),esk7_5(X16,X47,X48,X49,X50))
& leq(s(zero),esk7_5(X16,X47,X48,X49,X50))
& ~ setIn(esk7_5(X16,X47,X48,X49,X50),index(down,host(X50)))
& esk7_5(X16,X47,X48,X49,X50) != host(X49) )
| ~ elem(m_Down(X49),queue(host(X50)))
| host(X50) != host(X48)
| host(X50) != nbr_proc
| index(status,host(X50)) != elec_1
| ~ setIn(X47,alive)
| ~ elem(m_Down(X48),queue(host(X47))) )
& ! [X52,X53,X54,X55] :
( ~ setIn(X55,alive)
| ~ elem(m_Down(X54),queue(host(X55)))
| ~ elem(m_Ack(X55,X53),queue(host(X55)))
| ~ leq(nbr_proc,s(index(pendack,host(X55))))
| index(status,host(X55)) != elec_2
| host(X53) != index(pendack,host(X55))
| host(X54) != s(index(pendack,host(X55)))
| ~ setIn(X52,alive)
| index(ldr,host(X52)) != host(X52)
| index(status,host(X52)) != norm ) ) ),
inference(skolemize,[status(esa)],[190]) ).
fof(192,plain,
! [X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X52,X53,X54,X55] :
( ( ( ~ setIn(X55,alive)
| ~ elem(m_Down(X54),queue(host(X55)))
| ~ elem(m_Ack(X55,X53),queue(host(X55)))
| ~ leq(nbr_proc,s(index(pendack,host(X55))))
| index(status,host(X55)) != elec_2
| host(X53) != index(pendack,host(X55))
| host(X54) != s(index(pendack,host(X55)))
| ~ setIn(X52,alive)
| index(ldr,host(X52)) != host(X52)
| index(status,host(X52)) != norm )
& ( ( ~ leq(host(X50),esk7_5(X16,X47,X48,X49,X50))
& leq(s(zero),esk7_5(X16,X47,X48,X49,X50))
& ~ setIn(esk7_5(X16,X47,X48,X49,X50),index(down,host(X50)))
& esk7_5(X16,X47,X48,X49,X50) != host(X49) )
| ~ elem(m_Down(X49),queue(host(X50)))
| host(X50) != host(X48)
| host(X50) != nbr_proc
| index(status,host(X50)) != elec_1
| ~ setIn(X47,alive)
| ~ elem(m_Down(X48),queue(host(X47))) )
& ( leq(index(pendack,host(X46)),host(X44))
| ~ setIn(X46,alive)
| ~ elem(m_Halt(X46),queue(host(X45)))
| index(status,host(X46)) != elec_2
| ~ setIn(X44,alive)
| index(ldr,host(X44)) != host(X44)
| index(status,host(X44)) != norm )
& ( leq(host(X42),host(X43))
| ~ setIn(X42,alive)
| ~ setIn(X43,alive)
| index(status,host(X42)) != elec_2
| index(status,host(X43)) != elec_2
| ~ leq(index(pendack,host(X42)),index(pendack,host(X43))) )
& ( leq(host(X40),host(X41))
| ~ setIn(X40,alive)
| ~ setIn(X41,alive)
| index(status,host(X40)) != elec_2
| index(status,host(X41)) != elec_2
| leq(index(pendack,host(X41)),host(X40)) )
& ( ~ setIn(X37,alive)
| ~ setIn(X39,alive)
| host(X39) != host(X38)
| index(status,host(X37)) != elec_2
| index(status,host(X39)) != elec_2
| ~ elem(m_Ack(X37,X38),queue(host(X37))) )
& ( ~ setIn(X36,alive)
| ~ elem(m_Down(X35),queue(host(X36)))
| host(X35) != host(X34)
| ~ setIn(X34,alive)
| index(ldr,host(X34)) != host(X34)
| index(status,host(X34)) != norm )
& ( ( index(status,host(X33)) != elec_1
& index(status,host(X33)) != elec_2 )
| ~ setIn(X33,alive)
| index(elid,host(X33)) = X33 )
& ( ~ setIn(X32,alive)
| index(status,host(X32)) != elec_1
| ~ elem(m_Ack(X32,X31),queue(host(X32))) )
& ( ~ setIn(X30,alive)
| ~ elem(m_Ack(X30,X29),queue(host(X30)))
| leq(host(X29),index(pendack,host(X30))) )
& ( X28 = X27
| host(X28) != host(X27)
| ~ setIn(X27,alive)
| ~ setIn(X28,alive) )
& ( ~ elem(m_Ack(X26,X24),queue(host(X25)))
| ~ leq(host(X24),host(X26)) )
& ( ~ elem(m_Halt(X23),queue(host(X22)))
| ~ leq(host(X22),host(X23)) )
& ( ~ elem(m_Down(X21),queue(host(X20)))
| host(X21) != host(X20) )
& ( ~ elem(m_Ldr(X19),queue(host(X18)))
| ~ leq(host(X18),host(X19)) )
& ( host(X16) != host(X17)
| ~ setIn(X17,alive) ) )
| ~ epred1_1(X16) ),
inference(shift_quantors,[status(thm)],[191]) ).
fof(193,plain,
! [X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X52,X53,X54,X55] :
( ( ~ setIn(X55,alive)
| ~ elem(m_Down(X54),queue(host(X55)))
| ~ elem(m_Ack(X55,X53),queue(host(X55)))
| ~ leq(nbr_proc,s(index(pendack,host(X55))))
| index(status,host(X55)) != elec_2
| host(X53) != index(pendack,host(X55))
| host(X54) != s(index(pendack,host(X55)))
| ~ setIn(X52,alive)
| index(ldr,host(X52)) != host(X52)
| index(status,host(X52)) != norm
| ~ epred1_1(X16) )
& ( ~ leq(host(X50),esk7_5(X16,X47,X48,X49,X50))
| ~ elem(m_Down(X49),queue(host(X50)))
| host(X50) != host(X48)
| host(X50) != nbr_proc
| index(status,host(X50)) != elec_1
| ~ setIn(X47,alive)
| ~ elem(m_Down(X48),queue(host(X47)))
| ~ epred1_1(X16) )
& ( leq(s(zero),esk7_5(X16,X47,X48,X49,X50))
| ~ elem(m_Down(X49),queue(host(X50)))
| host(X50) != host(X48)
| host(X50) != nbr_proc
| index(status,host(X50)) != elec_1
| ~ setIn(X47,alive)
| ~ elem(m_Down(X48),queue(host(X47)))
| ~ epred1_1(X16) )
& ( ~ setIn(esk7_5(X16,X47,X48,X49,X50),index(down,host(X50)))
| ~ elem(m_Down(X49),queue(host(X50)))
| host(X50) != host(X48)
| host(X50) != nbr_proc
| index(status,host(X50)) != elec_1
| ~ setIn(X47,alive)
| ~ elem(m_Down(X48),queue(host(X47)))
| ~ epred1_1(X16) )
& ( esk7_5(X16,X47,X48,X49,X50) != host(X49)
| ~ elem(m_Down(X49),queue(host(X50)))
| host(X50) != host(X48)
| host(X50) != nbr_proc
| index(status,host(X50)) != elec_1
| ~ setIn(X47,alive)
| ~ elem(m_Down(X48),queue(host(X47)))
| ~ epred1_1(X16) )
& ( leq(index(pendack,host(X46)),host(X44))
| ~ setIn(X46,alive)
| ~ elem(m_Halt(X46),queue(host(X45)))
| index(status,host(X46)) != elec_2
| ~ setIn(X44,alive)
| index(ldr,host(X44)) != host(X44)
| index(status,host(X44)) != norm
| ~ epred1_1(X16) )
& ( leq(host(X42),host(X43))
| ~ setIn(X42,alive)
| ~ setIn(X43,alive)
| index(status,host(X42)) != elec_2
| index(status,host(X43)) != elec_2
| ~ leq(index(pendack,host(X42)),index(pendack,host(X43)))
| ~ epred1_1(X16) )
& ( leq(host(X40),host(X41))
| ~ setIn(X40,alive)
| ~ setIn(X41,alive)
| index(status,host(X40)) != elec_2
| index(status,host(X41)) != elec_2
| leq(index(pendack,host(X41)),host(X40))
| ~ epred1_1(X16) )
& ( ~ setIn(X37,alive)
| ~ setIn(X39,alive)
| host(X39) != host(X38)
| index(status,host(X37)) != elec_2
| index(status,host(X39)) != elec_2
| ~ elem(m_Ack(X37,X38),queue(host(X37)))
| ~ epred1_1(X16) )
& ( ~ setIn(X36,alive)
| ~ elem(m_Down(X35),queue(host(X36)))
| host(X35) != host(X34)
| ~ setIn(X34,alive)
| index(ldr,host(X34)) != host(X34)
| index(status,host(X34)) != norm
| ~ epred1_1(X16) )
& ( index(status,host(X33)) != elec_1
| ~ setIn(X33,alive)
| index(elid,host(X33)) = X33
| ~ epred1_1(X16) )
& ( index(status,host(X33)) != elec_2
| ~ setIn(X33,alive)
| index(elid,host(X33)) = X33
| ~ epred1_1(X16) )
& ( ~ setIn(X32,alive)
| index(status,host(X32)) != elec_1
| ~ elem(m_Ack(X32,X31),queue(host(X32)))
| ~ epred1_1(X16) )
& ( ~ setIn(X30,alive)
| ~ elem(m_Ack(X30,X29),queue(host(X30)))
| leq(host(X29),index(pendack,host(X30)))
| ~ epred1_1(X16) )
& ( X28 = X27
| host(X28) != host(X27)
| ~ setIn(X27,alive)
| ~ setIn(X28,alive)
| ~ epred1_1(X16) )
& ( ~ elem(m_Ack(X26,X24),queue(host(X25)))
| ~ leq(host(X24),host(X26))
| ~ epred1_1(X16) )
& ( ~ elem(m_Halt(X23),queue(host(X22)))
| ~ leq(host(X22),host(X23))
| ~ epred1_1(X16) )
& ( ~ elem(m_Down(X21),queue(host(X20)))
| host(X21) != host(X20)
| ~ epred1_1(X16) )
& ( ~ elem(m_Ldr(X19),queue(host(X18)))
| ~ leq(host(X18),host(X19))
| ~ epred1_1(X16) )
& ( host(X16) != host(X17)
| ~ setIn(X17,alive)
| ~ epred1_1(X16) ) ),
inference(distribute,[status(thm)],[192]) ).
cnf(213,plain,
( ~ epred1_1(X1)
| index(status,host(X2)) != norm
| index(ldr,host(X2)) != host(X2)
| ~ setIn(X2,alive)
| host(X3) != s(index(pendack,host(X4)))
| host(X5) != index(pendack,host(X4))
| index(status,host(X4)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(X4))))
| ~ elem(m_Ack(X4,X5),queue(host(X4)))
| ~ elem(m_Down(X3),queue(host(X4)))
| ~ setIn(X4,alive) ),
inference(split_conjunct,[status(thm)],[193]) ).
cnf(233,negated_conjecture,
leq(nbr_proc,s(host(esk4_0))),
inference(rw,[status(thm)],[179,175,theory(equality)]) ).
cnf(234,negated_conjecture,
s(host(esk4_0)) = host(esk5_0),
inference(rw,[status(thm)],[174,175,theory(equality)]) ).
cnf(236,negated_conjecture,
leq(nbr_proc,host(esk5_0)),
inference(rw,[status(thm)],[233,234,theory(equality)]) ).
cnf(315,negated_conjecture,
( m_Down(esk5_0) = m_Halt(esk1_0)
| elem(m_Down(esk5_0),queue(host(esk6_0))) ),
inference(spm,[status(thm)],[134,178,theory(equality)]) ).
cnf(316,negated_conjecture,
( m_Ack(esk6_0,esk4_0) = m_Halt(esk1_0)
| elem(m_Ack(esk6_0,esk4_0),queue(host(esk6_0))) ),
inference(spm,[status(thm)],[134,177,theory(equality)]) ).
cnf(318,negated_conjecture,
elem(m_Down(esk5_0),queue(host(esk6_0))),
inference(sr,[status(thm)],[315,61,theory(equality)]) ).
cnf(319,negated_conjecture,
elem(m_Ack(esk6_0,esk4_0),queue(host(esk6_0))),
inference(sr,[status(thm)],[316,64,theory(equality)]) ).
fof(396,plain,
( ~ epred16_0
<=> ! [X5,X3,X4] :
( ~ leq(nbr_proc,s(index(pendack,host(X4))))
| ~ elem(m_Down(X3),queue(host(X4)))
| ~ elem(m_Ack(X4,X5),queue(host(X4)))
| ~ setIn(X4,alive)
| index(status,host(X4)) != elec_2
| index(pendack,host(X4)) != host(X5)
| s(index(pendack,host(X4))) != host(X3) ) ),
introduced(definition),
[split] ).
cnf(397,plain,
( epred16_0
| ~ leq(nbr_proc,s(index(pendack,host(X4))))
| ~ elem(m_Down(X3),queue(host(X4)))
| ~ elem(m_Ack(X4,X5),queue(host(X4)))
| ~ setIn(X4,alive)
| index(status,host(X4)) != elec_2
| index(pendack,host(X4)) != host(X5)
| s(index(pendack,host(X4))) != host(X3) ),
inference(split_equiv,[status(thm)],[396]) ).
fof(398,plain,
( ~ epred17_0
<=> ! [X2] :
( ~ setIn(X2,alive)
| index(status,host(X2)) != norm
| index(ldr,host(X2)) != host(X2) ) ),
introduced(definition),
[split] ).
cnf(399,plain,
( epred17_0
| ~ setIn(X2,alive)
| index(status,host(X2)) != norm
| index(ldr,host(X2)) != host(X2) ),
inference(split_equiv,[status(thm)],[398]) ).
fof(400,plain,
( ~ epred18_0
<=> ! [X1] : ~ epred1_1(X1) ),
introduced(definition),
[split] ).
cnf(401,plain,
( epred18_0
| ~ epred1_1(X1) ),
inference(split_equiv,[status(thm)],[400]) ).
cnf(402,plain,
( ~ epred18_0
| ~ epred17_0
| ~ epred16_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[213,396,theory(equality)]),398,theory(equality)]),400,theory(equality)]),
[split] ).
cnf(415,negated_conjecture,
( host(esk5_0) = nbr_proc
| ~ leq(host(esk5_0),nbr_proc) ),
inference(spm,[status(thm)],[59,236,theory(equality)]) ).
cnf(417,negated_conjecture,
( host(esk5_0) = nbr_proc
| $false ),
inference(rw,[status(thm)],[415,116,theory(equality)]) ).
cnf(418,negated_conjecture,
host(esk5_0) = nbr_proc,
inference(cn,[status(thm)],[417,theory(equality)]) ).
cnf(457,negated_conjecture,
setIn(esk6_0,pids),
inference(spm,[status(thm)],[109,319,theory(equality)]) ).
cnf(476,negated_conjecture,
epred18_0,
inference(spm,[status(thm)],[401,169,theory(equality)]) ).
cnf(503,plain,
( $false
| ~ epred17_0
| ~ epred16_0 ),
inference(rw,[status(thm)],[402,476,theory(equality)]) ).
cnf(504,plain,
( ~ epred17_0
| ~ epred16_0 ),
inference(cn,[status(thm)],[503,theory(equality)]) ).
cnf(4313,negated_conjecture,
( epred16_0
| s(index(pendack,host(esk6_0))) != host(X1)
| index(pendack,host(esk6_0)) != host(esk4_0)
| index(status,host(esk6_0)) != elec_2
| ~ setIn(esk6_0,alive)
| ~ elem(m_Down(X1),queue(host(esk6_0)))
| ~ leq(nbr_proc,s(index(pendack,host(esk6_0)))) ),
inference(spm,[status(thm)],[397,319,theory(equality)]) ).
cnf(4316,negated_conjecture,
( epred16_0
| nbr_proc != host(X1)
| index(pendack,host(esk6_0)) != host(esk4_0)
| index(status,host(esk6_0)) != elec_2
| ~ setIn(esk6_0,alive)
| ~ elem(m_Down(X1),queue(host(esk6_0)))
| ~ leq(nbr_proc,s(index(pendack,host(esk6_0)))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[4313,175,theory(equality)]),234,theory(equality)]),418,theory(equality)]) ).
cnf(4317,negated_conjecture,
( epred16_0
| nbr_proc != host(X1)
| $false
| index(status,host(esk6_0)) != elec_2
| ~ setIn(esk6_0,alive)
| ~ elem(m_Down(X1),queue(host(esk6_0)))
| ~ leq(nbr_proc,s(index(pendack,host(esk6_0)))) ),
inference(rw,[status(thm)],[4316,175,theory(equality)]) ).
cnf(4318,negated_conjecture,
( epred16_0
| nbr_proc != host(X1)
| $false
| $false
| ~ setIn(esk6_0,alive)
| ~ elem(m_Down(X1),queue(host(esk6_0)))
| ~ leq(nbr_proc,s(index(pendack,host(esk6_0)))) ),
inference(rw,[status(thm)],[4317,176,theory(equality)]) ).
cnf(4319,negated_conjecture,
( epred16_0
| nbr_proc != host(X1)
| $false
| $false
| ~ setIn(esk6_0,alive)
| ~ elem(m_Down(X1),queue(host(esk6_0)))
| $false ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[4318,175,theory(equality)]),234,theory(equality)]),418,theory(equality)]),150,theory(equality)]) ).
cnf(4320,negated_conjecture,
( epred16_0
| nbr_proc != host(X1)
| ~ setIn(esk6_0,alive)
| ~ elem(m_Down(X1),queue(host(esk6_0))) ),
inference(cn,[status(thm)],[4319,theory(equality)]) ).
cnf(4407,negated_conjecture,
( epred17_0
| esk3_0 = esk1_0
| index(ldr,host(esk3_0)) != host(esk3_0)
| index(status,host(esk3_0)) != norm ),
inference(spm,[status(thm)],[399,173,theory(equality)]) ).
cnf(4409,negated_conjecture,
( epred17_0
| esk3_0 = esk1_0
| $false
| index(status,host(esk3_0)) != norm ),
inference(rw,[status(thm)],[4407,172,theory(equality)]) ).
cnf(4410,negated_conjecture,
( epred17_0
| esk3_0 = esk1_0
| $false
| $false ),
inference(rw,[status(thm)],[4409,171,theory(equality)]) ).
cnf(4411,negated_conjecture,
( epred17_0
| esk3_0 = esk1_0 ),
inference(cn,[status(thm)],[4410,theory(equality)]) ).
cnf(4415,negated_conjecture,
epred17_0,
inference(spm,[status(thm)],[183,4411,theory(equality)]) ).
cnf(4418,plain,
( $false
| ~ epred16_0 ),
inference(rw,[status(thm)],[504,4415,theory(equality)]) ).
cnf(4419,plain,
~ epred16_0,
inference(cn,[status(thm)],[4418,theory(equality)]) ).
cnf(299802,negated_conjecture,
( host(X1) != nbr_proc
| ~ setIn(esk6_0,alive)
| ~ elem(m_Down(X1),queue(host(esk6_0))) ),
inference(sr,[status(thm)],[4320,4419,theory(equality)]) ).
cnf(299803,negated_conjecture,
( host(esk5_0) != nbr_proc
| ~ setIn(esk6_0,alive) ),
inference(spm,[status(thm)],[299802,318,theory(equality)]) ).
cnf(299804,negated_conjecture,
( $false
| ~ setIn(esk6_0,alive) ),
inference(rw,[status(thm)],[299803,418,theory(equality)]) ).
cnf(299805,negated_conjecture,
~ setIn(esk6_0,alive),
inference(cn,[status(thm)],[299804,theory(equality)]) ).
cnf(299806,negated_conjecture,
esk6_0 = esk1_0,
inference(sr,[status(thm)],[180,299805,theory(equality)]) ).
cnf(299839,negated_conjecture,
setIn(esk1_0,pids),
inference(rw,[status(thm)],[457,299806,theory(equality)]) ).
cnf(299840,negated_conjecture,
$false,
inference(sr,[status(thm)],[299839,187,theory(equality)]) ).
cnf(299841,negated_conjecture,
$false,
299840,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% /home/graph/tptp/Systems/SInE---0.4/Source/sine.py:10: DeprecationWarning: the sets module is deprecated
% from sets import Set
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWV/SWV461+1.p
% --creating new selector for [SWV011+0.ax]
% -running prover on /tmp/tmpEAAMfW/sel_SWV461+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWV461+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWV/SWV461+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWV/SWV461+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------