%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV475+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:23:21 PM UTC 2026
% Result : Theorem 232.32s 145.70s
% Output : CNFRefutation 245.91s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_66)
% Comments :
%------------------------------------------------------------------------------
fof(conj,conjecture,
! [X12,X13,X5,X6] :
( ( ! [X7,X14] :
( elem(m_Ldr(X14),queue(host(X7)))
=> ~ leq(host(X7),host(X14)) )
& ! [X7,X14] :
( elem(m_Down(X14),queue(host(X7)))
=> host(X14) != host(X7) )
& ! [X7,X14] :
( ( X14 != X7
& host(X14) = host(X7) )
=> ( ~ setIn(X7,alive)
| ~ setIn(X14,alive) ) )
& ! [X7] :
( ( ( index(status,host(X7)) = elec_1
| index(status,host(X7)) = elec_2 )
& setIn(X7,alive) )
=> index(elid,host(X7)) = X7 )
& ! [X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& setIn(host(X14),index(down,host(X7)))
& index(status,host(X14)) = elec_2 )
=> leq(index(pendack,host(X14)),host(X7)) )
& ! [X7,X14] :
( ( setIn(X14,alive)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> ~ ( setIn(X7,alive)
& setIn(host(X14),index(down,host(X7))) ) )
& ! [X7,X15,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& elem(m_Down(X15),queue(host(X7)))
& host(X14) = host(X15)
& index(status,host(X14)) = elec_2 )
=> leq(index(pendack,host(X14)),host(X7)) )
& ! [X7,X15,X14] :
( ( setIn(X14,alive)
& host(X15) = host(X14)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> ~ ( setIn(X7,alive)
& elem(m_Down(X15),queue(host(X7))) ) )
& ! [X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> X14 = X7 )
& ! [X7,X15,X14] :
( ( ~ leq(host(X15),host(X14))
& setIn(X14,alive)
& elem(m_Down(X15),queue(host(X14)))
& host(X15) = host(X7) )
=> ~ ( setIn(X7,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm ) )
& ! [X7,X16,X15,X14] :
( ( host(X15) != host(X7)
& setIn(X7,alive)
& setIn(X15,alive)
& host(X16) = host(X7)
& host(X14) = host(X15) )
=> ~ ( elem(m_Down(X14),queue(host(X7)))
& elem(m_Down(X16),queue(host(X15))) ) )
& ! [X7,X16,X15,X14] :
( ( host(X15) != host(X7)
& setIn(X7,alive)
& setIn(X15,alive)
& host(X16) = host(X7)
& host(X14) = host(X15) )
=> ~ ( elem(m_Down(X14),queue(host(X7)))
& setIn(host(X16),index(down,host(X15))) ) )
& ! [X7,X15,X14] :
( ( host(X14) != host(X15)
& setIn(X14,alive)
& elem(m_Down(X7),queue(host(X14)))
& host(X15) = host(X7)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X15) )
=> ~ ( setIn(X15,alive)
& index(status,host(X15)) = norm
& index(ldr,host(X15)) = host(X15) ) )
& ! [X7,X15,X14] :
( ( host(X14) != host(X15)
& setIn(X14,alive)
& elem(m_Down(X7),queue(host(X14)))
& host(X15) = host(X7)
& index(status,host(X14)) = wait
& host(index(elid,host(X14))) = host(X15) )
=> ~ ( setIn(X15,alive)
& index(status,host(X15)) = norm
& index(ldr,host(X15)) = host(X15) ) )
& ! [X7,X16,X15,X14] :
( ( ! [X17] :
( ( ~ leq(host(X14),X17)
& leq(s(zero),X17) )
=> ( setIn(X17,index(down,host(X14)))
| X17 = host(X15) ) )
& setIn(X7,alive)
& leq(host(X7),host(X14))
& elem(m_Down(X15),queue(host(X14)))
& host(X16) = host(X14)
& index(status,host(X7)) = elec_2
& index(status,host(X14)) = elec_1 )
=> ~ elem(m_Ack(X7,X16),queue(host(X7))) )
& ! [X7,X16,X15,X14] :
( ( ! [X17] :
( ( ~ leq(host(X14),X17)
& leq(s(zero),X17) )
=> ( setIn(X17,index(down,host(X14)))
| X17 = host(X15) ) )
& setIn(X14,alive)
& leq(nbr_proc,s(host(X14)))
& elem(m_Down(X15),queue(host(X14)))
& elem(m_Down(X16),queue(host(X14)))
& host(X16) = s(host(X14))
& index(status,host(X14)) = elec_1 )
=> ~ ( setIn(X7,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm ) )
& queue(host(X5)) = cons(m_Ack(X13,X6),X12) )
=> ( setIn(X5,alive)
=> ( ( index(elid,host(X5)) = X13
& index(status,host(X5)) = elec_2
& host(X6) = index(pendack,host(X5)) )
=> ( leq(nbr_proc,index(pendack,host(X5)))
=> ! [X7] :
( ( setIn(host(X7),index(acks,host(X5)))
| host(X7) = host(X6) )
=> ! [X17] :
( host(X5) = host(X17)
=> ! [X18,X19,X20] :
( host(X7) = host(X20)
=> ( host(X5) != host(X20)
=> ( ( ! [X21] :
( ( ~ leq(host(X20),X21)
& leq(s(zero),X21) )
=> ( setIn(X21,index(down,host(X20)))
| X21 = host(X19) ) )
& setIn(X20,alive)
& leq(nbr_proc,s(host(X20)))
& elem(m_Down(X18),snoc(queue(host(X20)),m_Ldr(X5)))
& elem(m_Down(X19),snoc(queue(host(X20)),m_Ldr(X5)))
& host(X18) = s(host(X20))
& index(status,host(X20)) = elec_1 )
=> ~ ( setIn(X17,alive)
& host(X5) = host(X17) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
fof(axiom_58,axiom,
! [X5] : ~ leq(s(X5),X5),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_58) ).
fof(axiom_65,axiom,
! [X5] : ~ setIn(X5,setEmpty),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_65) ).
fof(axiom_45,axiom,
! [X5] : ~ elem(X5,q_nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_45) ).
fof(axiom_54,axiom,
! [X5,X4] :
( ordered(snoc(X4,X5))
<=> ( ordered(X4)
& ! [X6] :
( ( elem(X6,X4)
& pidElem(X5)
& pidElem(X6)
& host(pidMsg(X6)) = host(pidMsg(X5)) )
=> leq(pidMsg(X6),pidMsg(X5)) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_54) ).
fof(axiom_53,axiom,
! [X5,X4] :
( ordered(cons(X5,X4))
<=> ( ordered(X4)
& ! [X6] :
( ( elem(X6,X4)
& pidElem(X5)
& pidElem(X6)
& host(pidMsg(X6)) = host(pidMsg(X5)) )
=> leq(pidMsg(X5),pidMsg(X6)) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_53) ).
fof(axiom_57,axiom,
! [X4,X5,X6] :
( ( ordered(cons(m_Halt(X5),X4))
& host(X5) = host(X6)
& elem(m_Down(X6),X4) )
=> leq(X5,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_57) ).
fof(axiom,axiom,
! [X1,X2] :
( elem(m_Ack(X1,X2),queue(host(X1)))
=> ( setIn(X1,pids)
& setIn(X2,pids) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom) ).
fof(axiom_55,axiom,
! [X4,X5,X6] :
( ordered(X4)
=> ordered(snoc(X4,m_Ack(X5,X6))) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_55) ).
fof(axiom_46,axiom,
! [X5,X6,X4] :
( elem(X5,cons(X6,X4))
<=> ( X5 = X6
| elem(X5,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_46) ).
fof(axiom_47,axiom,
! [X5,X6,X4] :
( elem(X5,snoc(X4,X6))
<=> ( X5 = X6
| elem(X5,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_47) ).
fof(axiom_44,axiom,
! [X5,X6,X4] : snoc(cons(X5,X4),X6) = cons(X5,snoc(X4,X6)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_44) ).
fof(axiom_62,axiom,
! [X5,X6,X7] :
( ( leq(X5,X6)
& leq(X6,X7) )
=> leq(X5,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_62) ).
fof(axiom_63,axiom,
! [X5,X6] :
( leq(X5,X6)
<=> leq(s(X5),s(X6)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_63) ).
fof(axiom_64,axiom,
! [X5,X6] :
( leq(X5,s(X6))
<=> ( X5 = s(X6)
| leq(X5,X6) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_64) ).
fof(axiom_56,axiom,
! [X4,X5] :
( ordered(X4)
=> ordered(snoc(X4,m_Ldr(X5))) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_56) ).
fof(axiom_61,axiom,
! [X5,X6] :
( ( leq(X5,X6)
& leq(X6,X5) )
<=> X5 = X6 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_61) ).
fof(axiom_31,axiom,
! [X8,X9,X10,X11] :
( X8 != X9
=> m_Ack(X8,X10) != m_Ack(X9,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_31) ).
fof(axiom_32,axiom,
! [X8,X9,X10,X11] :
( X10 != X11
=> m_Ack(X8,X10) != m_Ack(X9,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_32) ).
fof(axiom_01,axiom,
! [X3,X4] :
( s(host(X3)) = host(X4)
=> host(X3) != host(X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_01) ).
fof(axiom_38,axiom,
! [X6,X4] : init(snoc(X4,X6)) = X4,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_38) ).
fof(axiom_37,axiom,
! [X6,X4] : last(snoc(X4,X6)) = X6,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_37) ).
fof(axiom_36,axiom,
! [X5,X4] : tail(cons(X5,X4)) = X4,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_36) ).
fof(axiom_35,axiom,
! [X5,X4] : head(cons(X5,X4)) = X5,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_35) ).
fof(axiom_48,axiom,
! [X5] :
( pidElem(X5)
<=> ? [X6] :
( X5 = m_Halt(X6)
| X5 = m_Down(X6) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_48) ).
fof(axiom_60,axiom,
! [X5,X6] :
( leq(X5,X6)
| leq(X6,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_60) ).
fof(axiom_40,axiom,
! [X4] :
( X4 = q_nil
| X4 = snoc(init(X4),last(X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_40) ).
fof(axiom_39,axiom,
! [X4] :
( X4 = q_nil
| X4 = cons(head(X4),tail(X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_39) ).
fof(axiom_15,axiom,
! [X5,X6,X7] : m_Ack(X5,X6) != m_NormQ(X7),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_15) ).
fof(axiom_14,axiom,
! [X5,X6,X7] : m_Ack(X5,X6) != m_Ldr(X7),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_14) ).
fof(axiom_13,axiom,
! [X5,X6,X7] : m_Ack(X5,X6) != m_NotNorm(X7),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_13) ).
fof(axiom_12,axiom,
! [X5,X6,X7] : m_Ack(X5,X6) != m_Down(X7),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_12) ).
fof(axiom_11,axiom,
! [X5,X6,X7] : m_Ack(X5,X6) != m_Halt(X7),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_11) ).
fof(axiom_52,axiom,
! [X5] :
( ordered(cons(X5,q_nil))
& ordered(snoc(q_nil,X5)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_52) ).
fof(axiom_43,axiom,
! [X5] : cons(X5,q_nil) = snoc(q_nil,X5),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_43) ).
fof(axiom_02,axiom,
! [X3] : leq(s(zero),host(X3)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_02) ).
fof(axiom_42,axiom,
! [X6,X4] : q_nil != snoc(X4,X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_42) ).
fof(axiom_41,axiom,
! [X5,X4] : q_nil != cons(X5,X4),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_41) ).
fof(axiom_04,axiom,
! [X3] : leq(host(X3),nbr_proc),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_04) ).
fof(axiom_34,axiom,
~ setIn(nil,alive),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_34) ).
fof(axiom_27,axiom,
! [X5,X6] :
( X5 != X6
<=> m_NormQ(X5) != m_NormQ(X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_27) ).
fof(axiom_29,axiom,
! [X5,X6] :
( X5 != X6
<=> m_Ldr(X5) != m_Ldr(X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_29) ).
fof(axiom_28,axiom,
! [X5,X6] :
( X5 != X6
<=> m_NotNorm(X5) != m_NotNorm(X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_28) ).
fof(axiom_30,axiom,
! [X5,X6] :
( X5 != X6
<=> m_Down(X5) != m_Down(X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_30) ).
fof(axiom_26,axiom,
! [X5,X6] :
( X5 != X6
<=> m_Halt(X5) != m_Halt(X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_26) ).
fof(axiom_59,axiom,
! [X5] : leq(X5,X5),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_59) ).
fof(axiom_25,axiom,
! [X5,X6] : m_NormQ(X5) != m_NotNorm(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_25) ).
fof(axiom_21,axiom,
! [X5,X6] : m_NormQ(X5) != m_Halt(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_21) ).
fof(axiom_23,axiom,
! [X5,X6] : m_Ldr(X5) != m_NormQ(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_23) ).
fof(axiom_20,axiom,
! [X5,X6] : m_Down(X5) != m_NormQ(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_20) ).
fof(axiom_24,axiom,
! [X5,X6] : m_Ldr(X5) != m_NotNorm(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_24) ).
fof(axiom_22,axiom,
! [X5,X6] : m_Ldr(X5) != m_Halt(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_22) ).
fof(axiom_18,axiom,
! [X5,X6] : m_Down(X5) != m_Ldr(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_18) ).
fof(axiom_16,axiom,
! [X5,X6] : m_NotNorm(X5) != m_Halt(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_16) ).
fof(axiom_19,axiom,
! [X5,X6] : m_Down(X5) != m_NotNorm(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_19) ).
fof(axiom_17,axiom,
! [X5,X6] : m_Down(X5) != m_Halt(X6),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_17) ).
fof(axiom_50,axiom,
! [X5] : pidMsg(m_Down(X5)) = X5,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_50) ).
fof(axiom_49,axiom,
! [X5] : pidMsg(m_Halt(X5)) = X5,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_49) ).
fof(axiom_03,axiom,
leq(s(zero),nbr_proc),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_03) ).
fof(axiom_51,axiom,
ordered(q_nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_51) ).
fof(axiom_10,axiom,
norm != wait,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_10) ).
fof(axiom_09,axiom,
elec_2 != norm,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_09) ).
fof(axiom_07,axiom,
elec_1 != norm,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_07) ).
fof(axiom_08,axiom,
elec_2 != wait,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_08) ).
fof(axiom_06,axiom,
elec_1 != wait,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_06) ).
fof(axiom_05,axiom,
elec_1 != elec_2,
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_05) ).
fof(i_0_66,plain,
! [X13,X5,X6,X12] :
( epred1_4(X12,X6,X5,X13)
<=> ( ! [X7,X14] :
( elem(m_Ldr(X14),queue(host(X7)))
=> ~ leq(host(X7),host(X14)) )
& ! [X7,X14] :
( elem(m_Down(X14),queue(host(X7)))
=> host(X14) != host(X7) )
& ! [X7,X14] :
( ( X14 != X7
& host(X14) = host(X7) )
=> ( ~ setIn(X7,alive)
| ~ setIn(X14,alive) ) )
& ! [X7] :
( ( ( index(status,host(X7)) = elec_1
| index(status,host(X7)) = elec_2 )
& setIn(X7,alive) )
=> index(elid,host(X7)) = X7 )
& ! [X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& setIn(host(X14),index(down,host(X7)))
& index(status,host(X14)) = elec_2 )
=> leq(index(pendack,host(X14)),host(X7)) )
& ! [X7,X14] :
( ( setIn(X14,alive)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> ~ ( setIn(X7,alive)
& setIn(host(X14),index(down,host(X7))) ) )
& ! [X7,X15,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& elem(m_Down(X15),queue(host(X7)))
& host(X14) = host(X15)
& index(status,host(X14)) = elec_2 )
=> leq(index(pendack,host(X14)),host(X7)) )
& ! [X7,X15,X14] :
( ( setIn(X14,alive)
& host(X15) = host(X14)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> ~ ( setIn(X7,alive)
& elem(m_Down(X15),queue(host(X7))) ) )
& ! [X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> X14 = X7 )
& ! [X7,X15,X14] :
( ( ~ leq(host(X15),host(X14))
& setIn(X14,alive)
& elem(m_Down(X15),queue(host(X14)))
& host(X15) = host(X7) )
=> ~ ( setIn(X7,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm ) )
& ! [X7,X16,X15,X14] :
( ( host(X15) != host(X7)
& setIn(X7,alive)
& setIn(X15,alive)
& host(X16) = host(X7)
& host(X14) = host(X15) )
=> ~ ( elem(m_Down(X14),queue(host(X7)))
& elem(m_Down(X16),queue(host(X15))) ) )
& ! [X7,X16,X15,X14] :
( ( host(X15) != host(X7)
& setIn(X7,alive)
& setIn(X15,alive)
& host(X16) = host(X7)
& host(X14) = host(X15) )
=> ~ ( elem(m_Down(X14),queue(host(X7)))
& setIn(host(X16),index(down,host(X15))) ) )
& ! [X7,X15,X14] :
( ( host(X14) != host(X15)
& setIn(X14,alive)
& elem(m_Down(X7),queue(host(X14)))
& host(X15) = host(X7)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X15) )
=> ~ ( setIn(X15,alive)
& index(status,host(X15)) = norm
& index(ldr,host(X15)) = host(X15) ) )
& ! [X7,X15,X14] :
( ( host(X14) != host(X15)
& setIn(X14,alive)
& elem(m_Down(X7),queue(host(X14)))
& host(X15) = host(X7)
& index(status,host(X14)) = wait
& host(index(elid,host(X14))) = host(X15) )
=> ~ ( setIn(X15,alive)
& index(status,host(X15)) = norm
& index(ldr,host(X15)) = host(X15) ) )
& ! [X7,X16,X15,X14] :
( ( ! [X17] :
( ( ~ leq(host(X14),X17)
& leq(s(zero),X17) )
=> ( setIn(X17,index(down,host(X14)))
| X17 = host(X15) ) )
& setIn(X7,alive)
& leq(host(X7),host(X14))
& elem(m_Down(X15),queue(host(X14)))
& host(X16) = host(X14)
& index(status,host(X7)) = elec_2
& index(status,host(X14)) = elec_1 )
=> ~ elem(m_Ack(X7,X16),queue(host(X7))) )
& ! [X7,X16,X15,X14] :
( ( ! [X17] :
( ( ~ leq(host(X14),X17)
& leq(s(zero),X17) )
=> ( setIn(X17,index(down,host(X14)))
| X17 = host(X15) ) )
& setIn(X14,alive)
& leq(nbr_proc,s(host(X14)))
& elem(m_Down(X15),queue(host(X14)))
& elem(m_Down(X16),queue(host(X14)))
& host(X16) = s(host(X14))
& index(status,host(X14)) = elec_1 )
=> ~ ( setIn(X7,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm ) )
& queue(host(X5)) = cons(m_Ack(X13,X6),X12) ) ),
introduced(definition) ).
fof(i_0_67,plain,
! [X13,X5,X6,X12] :
( epred1_4(X12,X6,X5,X13)
=> ( ! [X7,X14] :
( elem(m_Ldr(X14),queue(host(X7)))
=> ~ leq(host(X7),host(X14)) )
& ! [X7,X14] :
( elem(m_Down(X14),queue(host(X7)))
=> host(X14) != host(X7) )
& ! [X7,X14] :
( ( X14 != X7
& host(X14) = host(X7) )
=> ( ~ setIn(X7,alive)
| ~ setIn(X14,alive) ) )
& ! [X7] :
( ( ( index(status,host(X7)) = elec_1
| index(status,host(X7)) = elec_2 )
& setIn(X7,alive) )
=> index(elid,host(X7)) = X7 )
& ! [X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& setIn(host(X14),index(down,host(X7)))
& index(status,host(X14)) = elec_2 )
=> leq(index(pendack,host(X14)),host(X7)) )
& ! [X7,X14] :
( ( setIn(X14,alive)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> ~ ( setIn(X7,alive)
& setIn(host(X14),index(down,host(X7))) ) )
& ! [X7,X15,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& elem(m_Down(X15),queue(host(X7)))
& host(X14) = host(X15)
& index(status,host(X14)) = elec_2 )
=> leq(index(pendack,host(X14)),host(X7)) )
& ! [X7,X15,X14] :
( ( setIn(X14,alive)
& host(X15) = host(X14)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> ~ ( setIn(X7,alive)
& elem(m_Down(X15),queue(host(X7))) ) )
& ! [X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X14) )
=> X14 = X7 )
& ! [X7,X15,X14] :
( ( ~ leq(host(X15),host(X14))
& setIn(X14,alive)
& elem(m_Down(X15),queue(host(X14)))
& host(X15) = host(X7) )
=> ~ ( setIn(X7,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm ) )
& ! [X7,X16,X15,X14] :
( ( host(X15) != host(X7)
& setIn(X7,alive)
& setIn(X15,alive)
& host(X16) = host(X7)
& host(X14) = host(X15) )
=> ~ ( elem(m_Down(X14),queue(host(X7)))
& elem(m_Down(X16),queue(host(X15))) ) )
& ! [X7,X16,X15,X14] :
( ( host(X15) != host(X7)
& setIn(X7,alive)
& setIn(X15,alive)
& host(X16) = host(X7)
& host(X14) = host(X15) )
=> ~ ( elem(m_Down(X14),queue(host(X7)))
& setIn(host(X16),index(down,host(X15))) ) )
& ! [X7,X15,X14] :
( ( host(X14) != host(X15)
& setIn(X14,alive)
& elem(m_Down(X7),queue(host(X14)))
& host(X15) = host(X7)
& index(status,host(X14)) = norm
& index(ldr,host(X14)) = host(X15) )
=> ~ ( setIn(X15,alive)
& index(status,host(X15)) = norm
& index(ldr,host(X15)) = host(X15) ) )
& ! [X7,X15,X14] :
( ( host(X14) != host(X15)
& setIn(X14,alive)
& elem(m_Down(X7),queue(host(X14)))
& host(X15) = host(X7)
& index(status,host(X14)) = wait
& host(index(elid,host(X14))) = host(X15) )
=> ~ ( setIn(X15,alive)
& index(status,host(X15)) = norm
& index(ldr,host(X15)) = host(X15) ) )
& ! [X7,X16,X15,X14] :
( ( ! [X17] :
( ( ~ leq(host(X14),X17)
& leq(s(zero),X17) )
=> ( setIn(X17,index(down,host(X14)))
| X17 = host(X15) ) )
& setIn(X7,alive)
& leq(host(X7),host(X14))
& elem(m_Down(X15),queue(host(X14)))
& host(X16) = host(X14)
& index(status,host(X7)) = elec_2
& index(status,host(X14)) = elec_1 )
=> ~ elem(m_Ack(X7,X16),queue(host(X7))) )
& ! [X7,X16,X15,X14] :
( ( ! [X17] :
( ( ~ leq(host(X14),X17)
& leq(s(zero),X17) )
=> ( setIn(X17,index(down,host(X14)))
| X17 = host(X15) ) )
& setIn(X14,alive)
& leq(nbr_proc,s(host(X14)))
& elem(m_Down(X15),queue(host(X14)))
& elem(m_Down(X16),queue(host(X14)))
& host(X16) = s(host(X14))
& index(status,host(X14)) = elec_1 )
=> ~ ( setIn(X7,alive)
& index(ldr,host(X7)) = host(X7)
& index(status,host(X7)) = norm ) )
& queue(host(X5)) = cons(m_Ack(X13,X6),X12) ) ),
inference(split_equiv,[status(thm)],[i_0_66]) ).
fof(i_0_68,negated_conjecture,
~ ! [X12,X13,X5,X6] :
( epred1_4(X12,X6,X5,X13)
=> ( setIn(X5,alive)
=> ( ( index(elid,host(X5)) = X13
& index(status,host(X5)) = elec_2
& host(X6) = index(pendack,host(X5)) )
=> ( leq(nbr_proc,index(pendack,host(X5)))
=> ! [X7] :
( ( setIn(host(X7),index(acks,host(X5)))
| host(X7) = host(X6) )
=> ! [X17] :
( host(X5) = host(X17)
=> ! [X18,X19,X20] :
( host(X7) = host(X20)
=> ( host(X5) != host(X20)
=> ( ( ! [X21] :
( ( ~ leq(host(X20),X21)
& leq(s(zero),X21) )
=> ( setIn(X21,index(down,host(X20)))
| X21 = host(X19) ) )
& setIn(X20,alive)
& leq(nbr_proc,s(host(X20)))
& elem(m_Down(X18),snoc(queue(host(X20)),m_Ldr(X5)))
& elem(m_Down(X19),snoc(queue(host(X20)),m_Ldr(X5)))
& host(X18) = s(host(X20))
& index(status,host(X20)) = elec_1 )
=> ~ ( setIn(X17,alive)
& host(X5) = host(X17) ) ) ) ) ) ) ) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj])]),c_0_66]) ).
fof(i_0_69,plain,
! [X5] : ~ leq(s(X5),X5),
inference(fof_simplification,[status(thm)],[axiom_58]) ).
fof(i_0_70,plain,
! [X5] : ~ setIn(X5,setEmpty),
inference(fof_simplification,[status(thm)],[axiom_65]) ).
fof(i_0_71,plain,
! [X5] : ~ elem(X5,q_nil),
inference(fof_simplification,[status(thm)],[axiom_45]) ).
fof(i_0_72,plain,
! [X336,X337,X338,X339,X340,X341,X342,X343,X344,X345,X346,X347,X348,X349,X350,X351,X352,X353,X354,X355,X356,X357,X358,X359,X360,X361,X362,X363,X364,X365,X366,X367,X368,X369,X370,X371,X372,X373,X374,X375,X376,X377,X378,X379,X381,X382,X383,X384] :
( ( ~ elem(m_Ldr(X341),queue(host(X340)))
| ~ leq(host(X340),host(X341))
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ elem(m_Down(X343),queue(host(X342)))
| host(X343) != host(X342)
| ~ epred1_4(X339,X338,X337,X336) )
& ( X345 = X344
| host(X345) != host(X344)
| ~ setIn(X344,alive)
| ~ setIn(X345,alive)
| ~ epred1_4(X339,X338,X337,X336) )
& ( index(status,host(X346)) != elec_1
| ~ setIn(X346,alive)
| index(elid,host(X346)) = X346
| ~ epred1_4(X339,X338,X337,X336) )
& ( index(status,host(X346)) != elec_2
| ~ setIn(X346,alive)
| index(elid,host(X346)) = X346
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ setIn(X347,alive)
| ~ setIn(X348,alive)
| ~ setIn(host(X348),index(down,host(X347)))
| index(status,host(X348)) != elec_2
| leq(index(pendack,host(X348)),host(X347))
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ setIn(X350,alive)
| index(status,host(X350)) != norm
| index(ldr,host(X350)) != host(X350)
| ~ setIn(X349,alive)
| ~ setIn(host(X350),index(down,host(X349)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ setIn(X351,alive)
| ~ setIn(X353,alive)
| ~ elem(m_Down(X352),queue(host(X351)))
| host(X353) != host(X352)
| index(status,host(X353)) != elec_2
| leq(index(pendack,host(X353)),host(X351))
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ setIn(X356,alive)
| host(X355) != host(X356)
| index(status,host(X356)) != norm
| index(ldr,host(X356)) != host(X356)
| ~ setIn(X354,alive)
| ~ elem(m_Down(X355),queue(host(X354)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ setIn(X357,alive)
| ~ setIn(X358,alive)
| index(ldr,host(X357)) != host(X357)
| index(status,host(X357)) != norm
| index(status,host(X358)) != norm
| index(ldr,host(X358)) != host(X358)
| X358 = X357
| ~ epred1_4(X339,X338,X337,X336) )
& ( leq(host(X360),host(X361))
| ~ setIn(X361,alive)
| ~ elem(m_Down(X360),queue(host(X361)))
| host(X360) != host(X359)
| ~ setIn(X359,alive)
| index(ldr,host(X359)) != host(X359)
| index(status,host(X359)) != norm
| ~ epred1_4(X339,X338,X337,X336) )
& ( host(X364) = host(X362)
| ~ setIn(X362,alive)
| ~ setIn(X364,alive)
| host(X363) != host(X362)
| host(X365) != host(X364)
| ~ elem(m_Down(X365),queue(host(X362)))
| ~ elem(m_Down(X363),queue(host(X364)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( host(X368) = host(X366)
| ~ setIn(X366,alive)
| ~ setIn(X368,alive)
| host(X367) != host(X366)
| host(X369) != host(X368)
| ~ elem(m_Down(X369),queue(host(X366)))
| ~ setIn(host(X367),index(down,host(X368)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( host(X372) = host(X371)
| ~ setIn(X372,alive)
| ~ elem(m_Down(X370),queue(host(X372)))
| host(X371) != host(X370)
| index(status,host(X372)) != norm
| index(ldr,host(X372)) != host(X371)
| ~ setIn(X371,alive)
| index(status,host(X371)) != norm
| index(ldr,host(X371)) != host(X371)
| ~ epred1_4(X339,X338,X337,X336) )
& ( host(X375) = host(X374)
| ~ setIn(X375,alive)
| ~ elem(m_Down(X373),queue(host(X375)))
| host(X374) != host(X373)
| index(status,host(X375)) != wait
| host(index(elid,host(X375))) != host(X374)
| ~ setIn(X374,alive)
| index(status,host(X374)) != norm
| index(ldr,host(X374)) != host(X374)
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ leq(host(X379),esk14_8(X336,X337,X338,X339,X376,X377,X378,X379))
| ~ setIn(X376,alive)
| ~ leq(host(X376),host(X379))
| ~ elem(m_Down(X378),queue(host(X379)))
| host(X377) != host(X379)
| index(status,host(X376)) != elec_2
| index(status,host(X379)) != elec_1
| ~ elem(m_Ack(X376,X377),queue(host(X376)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( leq(s(zero),esk14_8(X336,X337,X338,X339,X376,X377,X378,X379))
| ~ setIn(X376,alive)
| ~ leq(host(X376),host(X379))
| ~ elem(m_Down(X378),queue(host(X379)))
| host(X377) != host(X379)
| index(status,host(X376)) != elec_2
| index(status,host(X379)) != elec_1
| ~ elem(m_Ack(X376,X377),queue(host(X376)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ setIn(esk14_8(X336,X337,X338,X339,X376,X377,X378,X379),index(down,host(X379)))
| ~ setIn(X376,alive)
| ~ leq(host(X376),host(X379))
| ~ elem(m_Down(X378),queue(host(X379)))
| host(X377) != host(X379)
| index(status,host(X376)) != elec_2
| index(status,host(X379)) != elec_1
| ~ elem(m_Ack(X376,X377),queue(host(X376)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( esk14_8(X336,X337,X338,X339,X376,X377,X378,X379) != host(X378)
| ~ setIn(X376,alive)
| ~ leq(host(X376),host(X379))
| ~ elem(m_Down(X378),queue(host(X379)))
| host(X377) != host(X379)
| index(status,host(X376)) != elec_2
| index(status,host(X379)) != elec_1
| ~ elem(m_Ack(X376,X377),queue(host(X376)))
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ leq(host(X384),esk15_8(X336,X337,X338,X339,X381,X382,X383,X384))
| ~ setIn(X384,alive)
| ~ leq(nbr_proc,s(host(X384)))
| ~ elem(m_Down(X383),queue(host(X384)))
| ~ elem(m_Down(X382),queue(host(X384)))
| host(X382) != s(host(X384))
| index(status,host(X384)) != elec_1
| ~ setIn(X381,alive)
| index(ldr,host(X381)) != host(X381)
| index(status,host(X381)) != norm
| ~ epred1_4(X339,X338,X337,X336) )
& ( leq(s(zero),esk15_8(X336,X337,X338,X339,X381,X382,X383,X384))
| ~ setIn(X384,alive)
| ~ leq(nbr_proc,s(host(X384)))
| ~ elem(m_Down(X383),queue(host(X384)))
| ~ elem(m_Down(X382),queue(host(X384)))
| host(X382) != s(host(X384))
| index(status,host(X384)) != elec_1
| ~ setIn(X381,alive)
| index(ldr,host(X381)) != host(X381)
| index(status,host(X381)) != norm
| ~ epred1_4(X339,X338,X337,X336) )
& ( ~ setIn(esk15_8(X336,X337,X338,X339,X381,X382,X383,X384),index(down,host(X384)))
| ~ setIn(X384,alive)
| ~ leq(nbr_proc,s(host(X384)))
| ~ elem(m_Down(X383),queue(host(X384)))
| ~ elem(m_Down(X382),queue(host(X384)))
| host(X382) != s(host(X384))
| index(status,host(X384)) != elec_1
| ~ setIn(X381,alive)
| index(ldr,host(X381)) != host(X381)
| index(status,host(X381)) != norm
| ~ epred1_4(X339,X338,X337,X336) )
& ( esk15_8(X336,X337,X338,X339,X381,X382,X383,X384) != host(X383)
| ~ setIn(X384,alive)
| ~ leq(nbr_proc,s(host(X384)))
| ~ elem(m_Down(X383),queue(host(X384)))
| ~ elem(m_Down(X382),queue(host(X384)))
| host(X382) != s(host(X384))
| index(status,host(X384)) != elec_1
| ~ setIn(X381,alive)
| index(ldr,host(X381)) != host(X381)
| index(status,host(X381)) != norm
| ~ epred1_4(X339,X338,X337,X336) )
& ( queue(host(X337)) = cons(m_Ack(X336,X338),X339)
| ~ epred1_4(X339,X338,X337,X336) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_67])])])])]) ).
fof(i_0_73,negated_conjecture,
! [X335] :
( epred1_4(esk5_0,esk8_0,esk7_0,esk6_0)
& setIn(esk7_0,alive)
& index(elid,host(esk7_0)) = esk6_0
& index(status,host(esk7_0)) = elec_2
& host(esk8_0) = index(pendack,host(esk7_0))
& leq(nbr_proc,index(pendack,host(esk7_0)))
& ( setIn(host(esk9_0),index(acks,host(esk7_0)))
| host(esk9_0) = host(esk8_0) )
& host(esk7_0) = host(esk10_0)
& host(esk9_0) = host(esk13_0)
& host(esk7_0) != host(esk13_0)
& ( leq(host(esk13_0),X335)
| ~ leq(s(zero),X335)
| setIn(X335,index(down,host(esk13_0)))
| X335 = host(esk12_0) )
& setIn(esk13_0,alive)
& leq(nbr_proc,s(host(esk13_0)))
& elem(m_Down(esk11_0),snoc(queue(host(esk13_0)),m_Ldr(esk7_0)))
& elem(m_Down(esk12_0),snoc(queue(host(esk13_0)),m_Ldr(esk7_0)))
& host(esk11_0) = s(host(esk13_0))
& index(status,host(esk13_0)) = elec_1
& setIn(esk10_0,alive)
& host(esk7_0) = host(esk10_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_68])])])]) ).
fof(i_0_74,plain,
! [X298,X299,X300,X301,X302] :
( ( ordered(X299)
| ~ ordered(snoc(X299,X298)) )
& ( ~ elem(X300,X299)
| ~ pidElem(X298)
| ~ pidElem(X300)
| host(pidMsg(X300)) != host(pidMsg(X298))
| leq(pidMsg(X300),pidMsg(X298))
| ~ ordered(snoc(X299,X298)) )
& ( elem(esk4_2(X301,X302),X302)
| ~ ordered(X302)
| ordered(snoc(X302,X301)) )
& ( pidElem(X301)
| ~ ordered(X302)
| ordered(snoc(X302,X301)) )
& ( pidElem(esk4_2(X301,X302))
| ~ ordered(X302)
| ordered(snoc(X302,X301)) )
& ( host(pidMsg(esk4_2(X301,X302))) = host(pidMsg(X301))
| ~ ordered(X302)
| ordered(snoc(X302,X301)) )
& ( ~ leq(pidMsg(esk4_2(X301,X302)),pidMsg(X301))
| ~ ordered(X302)
| ordered(snoc(X302,X301)) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_54])])])])])]) ).
fof(i_0_75,plain,
! [X292,X293,X294,X295,X296] :
( ( ordered(X293)
| ~ ordered(cons(X292,X293)) )
& ( ~ elem(X294,X293)
| ~ pidElem(X292)
| ~ pidElem(X294)
| host(pidMsg(X294)) != host(pidMsg(X292))
| leq(pidMsg(X292),pidMsg(X294))
| ~ ordered(cons(X292,X293)) )
& ( elem(esk3_2(X295,X296),X296)
| ~ ordered(X296)
| ordered(cons(X295,X296)) )
& ( pidElem(X295)
| ~ ordered(X296)
| ordered(cons(X295,X296)) )
& ( pidElem(esk3_2(X295,X296))
| ~ ordered(X296)
| ordered(cons(X295,X296)) )
& ( host(pidMsg(esk3_2(X295,X296))) = host(pidMsg(X295))
| ~ ordered(X296)
| ordered(cons(X295,X296)) )
& ( ~ leq(pidMsg(X295),pidMsg(esk3_2(X295,X296)))
| ~ ordered(X296)
| ordered(cons(X295,X296)) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_53])])])])])]) ).
fof(i_0_76,plain,
! [X309,X310,X311] :
( ~ ordered(cons(m_Halt(X310),X309))
| host(X310) != host(X311)
| ~ elem(m_Down(X311),X309)
| leq(X310,X311) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_57])]) ).
fof(i_0_77,plain,
! [X197,X198] :
( ( setIn(X197,pids)
| ~ elem(m_Ack(X197,X198),queue(host(X197))) )
& ( setIn(X198,pids)
| ~ elem(m_Ack(X197,X198),queue(host(X197))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom])])]) ).
fof(i_0_78,plain,
! [X304,X305,X306] :
( ~ ordered(X304)
| ordered(snoc(X304,m_Ack(X305,X306))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_55])]) ).
fof(i_0_79,plain,
! [X277,X278,X279] :
( ( ~ elem(X277,cons(X278,X279))
| X277 = X278
| elem(X277,X279) )
& ( X277 != X278
| elem(X277,cons(X278,X279)) )
& ( ~ elem(X277,X279)
| elem(X277,cons(X278,X279)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_46])])]) ).
fof(i_0_80,plain,
! [X280,X281,X282] :
( ( ~ elem(X280,snoc(X282,X281))
| X280 = X281
| elem(X280,X282) )
& ( X280 != X281
| elem(X280,snoc(X282,X281)) )
& ( ~ elem(X280,X282)
| elem(X280,snoc(X282,X281)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_47])])]) ).
fof(i_0_81,plain,
! [X273,X274,X275] : snoc(cons(X273,X275),X274) = cons(X273,snoc(X275,X274)),
inference(variable_rename,[status(thm)],[axiom_44]) ).
fof(i_0_82,plain,
! [X318,X319,X320] :
( ~ leq(X318,X319)
| ~ leq(X319,X320)
| leq(X318,X320) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_62])]) ).
fof(i_0_83,plain,
! [X321,X322] :
( ( ~ leq(X321,X322)
| leq(s(X321),s(X322)) )
& ( ~ leq(s(X321),s(X322))
| leq(X321,X322) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_63])]) ).
fof(i_0_84,plain,
! [X323,X324] :
( ( ~ leq(X323,s(X324))
| X323 = s(X324)
| leq(X323,X324) )
& ( X323 != s(X324)
| leq(X323,s(X324)) )
& ( ~ leq(X323,X324)
| leq(X323,s(X324)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_64])])]) ).
fof(i_0_85,plain,
! [X307,X308] :
( ~ ordered(X307)
| ordered(snoc(X307,m_Ldr(X308))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_56])]) ).
fof(i_0_86,plain,
! [X316,X317] :
( ( ~ leq(X316,X317)
| ~ leq(X317,X316)
| X316 = X317 )
& ( leq(X316,X317)
| X316 != X317 )
& ( leq(X317,X316)
| X316 != X317 ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_61])])]) ).
fof(i_0_87,plain,
! [X248,X249,X250,X251] :
( X248 = X249
| m_Ack(X248,X250) != m_Ack(X249,X251) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_31])]) ).
fof(i_0_88,plain,
! [X252,X253,X254,X255] :
( X254 = X255
| m_Ack(X252,X254) != m_Ack(X253,X255) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_32])]) ).
fof(i_0_89,plain,
! [X199,X200] :
( s(host(X199)) != host(X200)
| host(X199) != host(X200) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_01])]) ).
fof(i_0_90,plain,
! [X312] : ~ leq(s(X312),X312),
inference(variable_rename,[status(thm)],[i_0_69]) ).
fof(i_0_91,plain,
! [X264,X265] : init(snoc(X265,X264)) = X265,
inference(variable_rename,[status(thm)],[axiom_38]) ).
fof(i_0_92,plain,
! [X262,X263] : last(snoc(X263,X262)) = X262,
inference(variable_rename,[status(thm)],[axiom_37]) ).
fof(i_0_93,plain,
! [X260,X261] : tail(cons(X260,X261)) = X261,
inference(variable_rename,[status(thm)],[axiom_36]) ).
fof(i_0_94,plain,
! [X258,X259] : head(cons(X258,X259)) = X258,
inference(variable_rename,[status(thm)],[axiom_35]) ).
fof(i_0_95,plain,
! [X283,X286,X287,X288] :
( ( ~ pidElem(X283)
| X283 = m_Halt(esk1_1(X283))
| X283 = m_Down(esk2_1(X283)) )
& ( X286 != m_Halt(X287)
| pidElem(X286) )
& ( X286 != m_Down(X288)
| pidElem(X286) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_48])])])])])]) ).
fof(i_0_96,plain,
! [X314,X315] :
( leq(X314,X315)
| leq(X315,X314) ),
inference(variable_rename,[status(thm)],[axiom_60]) ).
fof(i_0_97,plain,
! [X267] :
( X267 = q_nil
| X267 = snoc(init(X267),last(X267)) ),
inference(variable_rename,[status(thm)],[axiom_40]) ).
fof(i_0_98,plain,
! [X266] :
( X266 = q_nil
| X266 = cons(head(X266),tail(X266)) ),
inference(variable_rename,[status(thm)],[axiom_39]) ).
fof(i_0_99,plain,
! [X215,X216,X217] : m_Ack(X215,X216) != m_NormQ(X217),
inference(variable_rename,[status(thm)],[axiom_15]) ).
fof(i_0_100,plain,
! [X212,X213,X214] : m_Ack(X212,X213) != m_Ldr(X214),
inference(variable_rename,[status(thm)],[axiom_14]) ).
fof(i_0_101,plain,
! [X209,X210,X211] : m_Ack(X209,X210) != m_NotNorm(X211),
inference(variable_rename,[status(thm)],[axiom_13]) ).
fof(i_0_102,plain,
! [X206,X207,X208] : m_Ack(X206,X207) != m_Down(X208),
inference(variable_rename,[status(thm)],[axiom_12]) ).
fof(i_0_103,plain,
! [X203,X204,X205] : m_Ack(X203,X204) != m_Halt(X205),
inference(variable_rename,[status(thm)],[axiom_11]) ).
fof(i_0_104,plain,
! [X291] :
( ordered(cons(X291,q_nil))
& ordered(snoc(q_nil,X291)) ),
inference(variable_rename,[status(thm)],[axiom_52]) ).
fof(i_0_105,plain,
! [X272] : cons(X272,q_nil) = snoc(q_nil,X272),
inference(variable_rename,[status(thm)],[axiom_43]) ).
fof(i_0_106,plain,
! [X201] : leq(s(zero),host(X201)),
inference(variable_rename,[status(thm)],[axiom_02]) ).
fof(i_0_107,plain,
! [X270,X271] : q_nil != snoc(X271,X270),
inference(variable_rename,[status(thm)],[axiom_42]) ).
fof(i_0_108,plain,
! [X268,X269] : q_nil != cons(X268,X269),
inference(variable_rename,[status(thm)],[axiom_41]) ).
fof(i_0_109,plain,
! [X325] : ~ setIn(X325,setEmpty),
inference(variable_rename,[status(thm)],[i_0_70]) ).
fof(i_0_110,plain,
! [X276] : ~ elem(X276,q_nil),
inference(variable_rename,[status(thm)],[i_0_71]) ).
fof(i_0_111,plain,
! [X202] : leq(host(X202),nbr_proc),
inference(variable_rename,[status(thm)],[axiom_04]) ).
fof(i_0_112,plain,
~ setIn(nil,alive),
inference(fof_simplification,[status(thm)],[axiom_34]) ).
fof(i_0_113,plain,
! [X240,X241] :
( ( X240 = X241
| m_NormQ(X240) != m_NormQ(X241) )
& ( m_NormQ(X240) = m_NormQ(X241)
| X240 != X241 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_27])]) ).
fof(i_0_114,plain,
! [X244,X245] :
( ( X244 = X245
| m_Ldr(X244) != m_Ldr(X245) )
& ( m_Ldr(X244) = m_Ldr(X245)
| X244 != X245 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_29])]) ).
fof(i_0_115,plain,
! [X242,X243] :
( ( X242 = X243
| m_NotNorm(X242) != m_NotNorm(X243) )
& ( m_NotNorm(X242) = m_NotNorm(X243)
| X242 != X243 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_28])]) ).
fof(i_0_116,plain,
! [X246,X247] :
( ( X246 = X247
| m_Down(X246) != m_Down(X247) )
& ( m_Down(X246) = m_Down(X247)
| X246 != X247 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_30])]) ).
fof(i_0_117,plain,
! [X238,X239] :
( ( X238 = X239
| m_Halt(X238) != m_Halt(X239) )
& ( m_Halt(X238) = m_Halt(X239)
| X238 != X239 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_26])]) ).
fof(i_0_118,plain,
! [X313] : leq(X313,X313),
inference(variable_rename,[status(thm)],[axiom_59]) ).
fof(i_0_119,plain,
! [X236,X237] : m_NormQ(X236) != m_NotNorm(X237),
inference(variable_rename,[status(thm)],[axiom_25]) ).
fof(i_0_120,plain,
! [X228,X229] : m_NormQ(X228) != m_Halt(X229),
inference(variable_rename,[status(thm)],[axiom_21]) ).
fof(i_0_121,plain,
! [X232,X233] : m_Ldr(X232) != m_NormQ(X233),
inference(variable_rename,[status(thm)],[axiom_23]) ).
fof(i_0_122,plain,
! [X226,X227] : m_Down(X226) != m_NormQ(X227),
inference(variable_rename,[status(thm)],[axiom_20]) ).
fof(i_0_123,plain,
! [X234,X235] : m_Ldr(X234) != m_NotNorm(X235),
inference(variable_rename,[status(thm)],[axiom_24]) ).
fof(i_0_124,plain,
! [X230,X231] : m_Ldr(X230) != m_Halt(X231),
inference(variable_rename,[status(thm)],[axiom_22]) ).
fof(i_0_125,plain,
! [X222,X223] : m_Down(X222) != m_Ldr(X223),
inference(variable_rename,[status(thm)],[axiom_18]) ).
fof(i_0_126,plain,
! [X218,X219] : m_NotNorm(X218) != m_Halt(X219),
inference(variable_rename,[status(thm)],[axiom_16]) ).
fof(i_0_127,plain,
! [X224,X225] : m_Down(X224) != m_NotNorm(X225),
inference(variable_rename,[status(thm)],[axiom_19]) ).
fof(i_0_128,plain,
! [X220,X221] : m_Down(X220) != m_Halt(X221),
inference(variable_rename,[status(thm)],[axiom_17]) ).
fof(i_0_129,plain,
! [X290] : pidMsg(m_Down(X290)) = X290,
inference(variable_rename,[status(thm)],[axiom_50]) ).
fof(i_0_130,plain,
! [X289] : pidMsg(m_Halt(X289)) = X289,
inference(variable_rename,[status(thm)],[axiom_49]) ).
cnf(i_0_131,plain,
( ~ setIn(esk15_8(X1,X2,X3,X4,X5,X6,X7,X8),index(down,host(X8)))
| ~ setIn(X8,alive)
| ~ leq(nbr_proc,s(host(X8)))
| ~ elem(m_Down(X7),queue(host(X8)))
| ~ elem(m_Down(X6),queue(host(X8)))
| host(X6) != s(host(X8))
| index(status,host(X8)) != elec_1
| ~ setIn(X5,alive)
| index(ldr,host(X5)) != host(X5)
| index(status,host(X5)) != norm
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_132,plain,
( ~ setIn(esk14_8(X1,X2,X3,X4,X5,X6,X7,X8),index(down,host(X8)))
| ~ setIn(X5,alive)
| ~ leq(host(X5),host(X8))
| ~ elem(m_Down(X7),queue(host(X8)))
| host(X6) != host(X8)
| index(status,host(X5)) != elec_2
| index(status,host(X8)) != elec_1
| ~ elem(m_Ack(X5,X6),queue(host(X5)))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_133,plain,
( ~ leq(host(X1),esk15_8(X2,X3,X4,X5,X6,X7,X8,X1))
| ~ setIn(X1,alive)
| ~ leq(nbr_proc,s(host(X1)))
| ~ elem(m_Down(X8),queue(host(X1)))
| ~ elem(m_Down(X7),queue(host(X1)))
| host(X7) != s(host(X1))
| index(status,host(X1)) != elec_1
| ~ setIn(X6,alive)
| index(ldr,host(X6)) != host(X6)
| index(status,host(X6)) != norm
| ~ epred1_4(X5,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_134,plain,
( ~ leq(host(X1),esk14_8(X2,X3,X4,X5,X6,X7,X8,X1))
| ~ setIn(X6,alive)
| ~ leq(host(X6),host(X1))
| ~ elem(m_Down(X8),queue(host(X1)))
| host(X7) != host(X1)
| index(status,host(X6)) != elec_2
| index(status,host(X1)) != elec_1
| ~ elem(m_Ack(X6,X7),queue(host(X6)))
| ~ epred1_4(X5,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_135,plain,
( leq(s(zero),esk15_8(X1,X2,X3,X4,X5,X6,X7,X8))
| ~ setIn(X8,alive)
| ~ leq(nbr_proc,s(host(X8)))
| ~ elem(m_Down(X7),queue(host(X8)))
| ~ elem(m_Down(X6),queue(host(X8)))
| host(X6) != s(host(X8))
| index(status,host(X8)) != elec_1
| ~ setIn(X5,alive)
| index(ldr,host(X5)) != host(X5)
| index(status,host(X5)) != norm
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_136,plain,
( leq(s(zero),esk14_8(X1,X2,X3,X4,X5,X6,X7,X8))
| ~ setIn(X5,alive)
| ~ leq(host(X5),host(X8))
| ~ elem(m_Down(X7),queue(host(X8)))
| host(X6) != host(X8)
| index(status,host(X5)) != elec_2
| index(status,host(X8)) != elec_1
| ~ elem(m_Ack(X5,X6),queue(host(X5)))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_137,plain,
( esk15_8(X1,X2,X3,X4,X5,X6,X7,X8) != host(X7)
| ~ setIn(X8,alive)
| ~ leq(nbr_proc,s(host(X8)))
| ~ elem(m_Down(X7),queue(host(X8)))
| ~ elem(m_Down(X6),queue(host(X8)))
| host(X6) != s(host(X8))
| index(status,host(X8)) != elec_1
| ~ setIn(X5,alive)
| index(ldr,host(X5)) != host(X5)
| index(status,host(X5)) != norm
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_138,plain,
( esk14_8(X1,X2,X3,X4,X5,X6,X7,X8) != host(X7)
| ~ setIn(X5,alive)
| ~ leq(host(X5),host(X8))
| ~ elem(m_Down(X7),queue(host(X8)))
| host(X6) != host(X8)
| index(status,host(X5)) != elec_2
| index(status,host(X8)) != elec_1
| ~ elem(m_Ack(X5,X6),queue(host(X5)))
| ~ epred1_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_139,plain,
( host(X1) = host(X2)
| ~ setIn(X1,alive)
| ~ elem(m_Down(X3),queue(host(X1)))
| host(X2) != host(X3)
| index(status,host(X1)) != wait
| host(index(elid,host(X1))) != host(X2)
| ~ setIn(X2,alive)
| index(status,host(X2)) != norm
| index(ldr,host(X2)) != host(X2)
| ~ epred1_4(X4,X5,X6,X7) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_140,plain,
( host(X1) = host(X2)
| ~ setIn(X1,alive)
| ~ elem(m_Down(X3),queue(host(X1)))
| host(X2) != host(X3)
| index(status,host(X1)) != norm
| index(ldr,host(X1)) != host(X2)
| ~ setIn(X2,alive)
| index(status,host(X2)) != norm
| index(ldr,host(X2)) != host(X2)
| ~ epred1_4(X4,X5,X6,X7) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_141,plain,
( host(X1) = host(X2)
| ~ setIn(X2,alive)
| ~ setIn(X1,alive)
| host(X3) != host(X2)
| host(X4) != host(X1)
| ~ elem(m_Down(X4),queue(host(X2)))
| ~ setIn(host(X3),index(down,host(X1)))
| ~ epred1_4(X5,X6,X7,X8) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_142,plain,
( leq(index(pendack,host(X2)),host(X1))
| ~ setIn(X1,alive)
| ~ setIn(X2,alive)
| ~ setIn(host(X2),index(down,host(X1)))
| index(status,host(X2)) != elec_2
| ~ epred1_4(X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_143,plain,
( leq(host(X1),host(X2))
| ~ setIn(X2,alive)
| ~ elem(m_Down(X1),queue(host(X2)))
| host(X1) != host(X3)
| ~ setIn(X3,alive)
| index(ldr,host(X3)) != host(X3)
| index(status,host(X3)) != norm
| ~ epred1_4(X4,X5,X6,X7) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_144,plain,
( leq(index(pendack,host(X2)),host(X1))
| ~ setIn(X1,alive)
| ~ setIn(X2,alive)
| ~ elem(m_Down(X3),queue(host(X1)))
| host(X2) != host(X3)
| index(status,host(X2)) != elec_2
| ~ epred1_4(X4,X5,X6,X7) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_145,plain,
( host(X1) = host(X2)
| ~ setIn(X2,alive)
| ~ setIn(X1,alive)
| host(X3) != host(X2)
| host(X4) != host(X1)
| ~ elem(m_Down(X4),queue(host(X2)))
| ~ elem(m_Down(X3),queue(host(X1)))
| ~ epred1_4(X5,X6,X7,X8) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_146,plain,
( ~ setIn(X1,alive)
| index(status,host(X1)) != norm
| index(ldr,host(X1)) != host(X1)
| ~ setIn(X2,alive)
| ~ setIn(host(X1),index(down,host(X2)))
| ~ epred1_4(X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_147,plain,
( ~ setIn(X1,alive)
| host(X2) != host(X1)
| index(status,host(X1)) != norm
| index(ldr,host(X1)) != host(X1)
| ~ setIn(X3,alive)
| ~ elem(m_Down(X2),queue(host(X3)))
| ~ epred1_4(X4,X5,X6,X7) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_148,plain,
( X2 = X1
| ~ setIn(X1,alive)
| ~ setIn(X2,alive)
| index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm
| index(status,host(X2)) != norm
| index(ldr,host(X2)) != host(X2)
| ~ epred1_4(X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_149,plain,
( ~ elem(m_Ldr(X1),queue(host(X2)))
| ~ leq(host(X2),host(X1))
| ~ epred1_4(X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_150,plain,
( ~ elem(m_Down(X1),queue(host(X2)))
| host(X1) != host(X2)
| ~ epred1_4(X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_151,plain,
( index(elid,host(X1)) = X1
| index(status,host(X1)) != elec_2
| ~ setIn(X1,alive)
| ~ epred1_4(X2,X3,X4,X5) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_152,plain,
( index(elid,host(X1)) = X1
| index(status,host(X1)) != elec_1
| ~ setIn(X1,alive)
| ~ epred1_4(X2,X3,X4,X5) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_153,plain,
( X1 = X2
| host(X1) != host(X2)
| ~ setIn(X2,alive)
| ~ setIn(X1,alive)
| ~ epred1_4(X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_154,plain,
( queue(host(X1)) = cons(m_Ack(X2,X3),X4)
| ~ epred1_4(X4,X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_155,negated_conjecture,
epred1_4(esk5_0,esk8_0,esk7_0,esk6_0),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_156,plain,
( ordered(snoc(X2,X1))
| ~ leq(pidMsg(esk4_2(X1,X2)),pidMsg(X1))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_157,plain,
( ordered(cons(X1,X2))
| ~ leq(pidMsg(X1),pidMsg(esk3_2(X1,X2)))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_158,plain,
( leq(pidMsg(X1),pidMsg(X3))
| ~ elem(X1,X2)
| ~ pidElem(X3)
| ~ pidElem(X1)
| host(pidMsg(X1)) != host(pidMsg(X3))
| ~ ordered(snoc(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_159,plain,
( leq(pidMsg(X3),pidMsg(X1))
| ~ elem(X1,X2)
| ~ pidElem(X3)
| ~ pidElem(X1)
| host(pidMsg(X1)) != host(pidMsg(X3))
| ~ ordered(cons(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_160,plain,
( leq(X1,X3)
| ~ ordered(cons(m_Halt(X1),X2))
| host(X1) != host(X3)
| ~ elem(m_Down(X3),X2) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_161,plain,
( host(pidMsg(esk4_2(X1,X2))) = host(pidMsg(X1))
| ordered(snoc(X2,X1))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_162,plain,
( host(pidMsg(esk3_2(X1,X2))) = host(pidMsg(X1))
| ordered(cons(X1,X2))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_163,plain,
( setIn(X1,pids)
| ~ elem(m_Ack(X1,X2),queue(host(X1))) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_164,plain,
( setIn(X1,pids)
| ~ elem(m_Ack(X2,X1),queue(host(X2))) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_165,negated_conjecture,
( leq(host(esk13_0),X1)
| setIn(X1,index(down,host(esk13_0)))
| X1 = host(esk12_0)
| ~ leq(s(zero),X1) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_166,plain,
( ordered(snoc(X1,m_Ack(X2,X3)))
| ~ ordered(X1) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_167,plain,
( X1 = X2
| elem(X1,X3)
| ~ elem(X1,cons(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_168,plain,
( X1 = X3
| elem(X1,X2)
| ~ elem(X1,snoc(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_169,plain,
snoc(cons(X1,X2),X3) = cons(X1,snoc(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_170,plain,
( elem(esk4_2(X1,X2),X2)
| ordered(snoc(X2,X1))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_171,plain,
( elem(esk3_2(X1,X2),X2)
| ordered(cons(X1,X2))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_172,negated_conjecture,
elem(m_Down(esk12_0),snoc(queue(host(esk13_0)),m_Ldr(esk7_0))),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_173,negated_conjecture,
elem(m_Down(esk11_0),snoc(queue(host(esk13_0)),m_Ldr(esk7_0))),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_174,plain,
( pidElem(esk4_2(X1,X2))
| ordered(snoc(X2,X1))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_175,plain,
( pidElem(esk3_2(X1,X2))
| ordered(cons(X1,X2))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_176,plain,
( elem(X1,snoc(X2,X3))
| ~ elem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_177,plain,
( elem(X1,cons(X3,X2))
| ~ elem(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_178,plain,
( leq(X1,X3)
| ~ leq(X1,X2)
| ~ leq(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_179,plain,
( leq(X1,X2)
| ~ leq(s(X1),s(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_180,plain,
( ordered(X1)
| ~ ordered(snoc(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_181,plain,
( ordered(X1)
| ~ ordered(cons(X2,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_182,plain,
( X1 = s(X2)
| leq(X1,X2)
| ~ leq(X1,s(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_183,negated_conjecture,
( setIn(host(esk9_0),index(acks,host(esk7_0)))
| host(esk9_0) = host(esk8_0) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_184,plain,
( ordered(snoc(X1,m_Ldr(X2)))
| ~ ordered(X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_185,plain,
( leq(s(X1),s(X2))
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_186,plain,
( X1 = X2
| ~ leq(X1,X2)
| ~ leq(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_187,plain,
( X1 = X2
| m_Ack(X1,X3) != m_Ack(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_188,plain,
( X1 = X2
| m_Ack(X3,X1) != m_Ack(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_189,plain,
( elem(X1,snoc(X3,X2))
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_190,plain,
( elem(X1,cons(X2,X3))
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_191,plain,
( leq(X1,s(X2))
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_192,plain,
( pidElem(X1)
| ordered(snoc(X2,X1))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_193,plain,
( pidElem(X1)
| ordered(cons(X1,X2))
| ~ ordered(X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_194,negated_conjecture,
leq(nbr_proc,index(pendack,host(esk7_0))),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_195,plain,
( s(host(X1)) != host(X2)
| host(X1) != host(X2) ),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_196,plain,
~ leq(s(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_90]),
[final] ).
cnf(i_0_197,plain,
init(snoc(X1,X2)) = X1,
inference(split_conjunct,[status(thm)],[i_0_91]),
[final] ).
cnf(i_0_198,plain,
last(snoc(X1,X2)) = X2,
inference(split_conjunct,[status(thm)],[i_0_92]),
[final] ).
cnf(i_0_199,plain,
tail(cons(X1,X2)) = X2,
inference(split_conjunct,[status(thm)],[i_0_93]),
[final] ).
cnf(i_0_200,plain,
head(cons(X1,X2)) = X1,
inference(split_conjunct,[status(thm)],[i_0_94]),
[final] ).
cnf(i_0_201,plain,
( X1 = m_Halt(esk1_1(X1))
| X1 = m_Down(esk2_1(X1))
| ~ pidElem(X1) ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_202,plain,
( leq(X1,s(X2))
| X1 != s(X2) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_203,plain,
( leq(X1,X2)
| leq(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_204,plain,
( X1 = q_nil
| X1 = snoc(init(X1),last(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_97]),
[final] ).
cnf(i_0_205,plain,
( X1 = q_nil
| X1 = cons(head(X1),tail(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_206,plain,
m_Ack(X1,X2) != m_NormQ(X3),
inference(split_conjunct,[status(thm)],[i_0_99]),
[final] ).
cnf(i_0_207,plain,
m_Ack(X1,X2) != m_Ldr(X3),
inference(split_conjunct,[status(thm)],[i_0_100]),
[final] ).
cnf(i_0_208,plain,
m_Ack(X1,X2) != m_NotNorm(X3),
inference(split_conjunct,[status(thm)],[i_0_101]),
[final] ).
cnf(i_0_209,plain,
m_Ack(X1,X2) != m_Down(X3),
inference(split_conjunct,[status(thm)],[i_0_102]),
[final] ).
cnf(i_0_210,plain,
m_Ack(X1,X2) != m_Halt(X3),
inference(split_conjunct,[status(thm)],[i_0_103]),
[final] ).
cnf(i_0_211,plain,
ordered(snoc(q_nil,X1)),
inference(split_conjunct,[status(thm)],[i_0_104]),
[final] ).
cnf(i_0_212,plain,
ordered(cons(X1,q_nil)),
inference(split_conjunct,[status(thm)],[i_0_104]),
[final] ).
cnf(i_0_213,negated_conjecture,
leq(nbr_proc,s(host(esk13_0))),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_214,plain,
cons(X1,q_nil) = snoc(q_nil,X1),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_215,plain,
leq(s(zero),host(X1)),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_216,plain,
q_nil != snoc(X1,X2),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_217,plain,
q_nil != cons(X1,X2),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_218,plain,
~ setIn(X1,setEmpty),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_219,plain,
~ elem(X1,q_nil),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_220,plain,
leq(host(X1),nbr_proc),
inference(split_conjunct,[status(thm)],[i_0_111]),
[final] ).
cnf(i_0_221,negated_conjecture,
host(esk8_0) = index(pendack,host(esk7_0)),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_222,plain,
( leq(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_223,plain,
( leq(X1,X2)
| X2 != X1 ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_224,plain,
~ setIn(nil,alive),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_225,plain,
leq(s(zero),nbr_proc),
inference(split_conjunct,[status(thm)],[axiom_03]),
[final] ).
cnf(i_0_226,negated_conjecture,
index(elid,host(esk7_0)) = esk6_0,
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_227,negated_conjecture,
index(status,host(esk13_0)) = elec_1,
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_228,negated_conjecture,
index(status,host(esk7_0)) = elec_2,
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_229,plain,
( X1 = X2
| m_NormQ(X1) != m_NormQ(X2) ),
inference(split_conjunct,[status(thm)],[i_0_113]),
[final] ).
cnf(i_0_230,plain,
( X1 = X2
| m_Ldr(X1) != m_Ldr(X2) ),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_231,plain,
( X1 = X2
| m_NotNorm(X1) != m_NotNorm(X2) ),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_232,plain,
( X1 = X2
| m_Down(X1) != m_Down(X2) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_233,plain,
( X1 = X2
| m_Halt(X1) != m_Halt(X2) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_234,plain,
leq(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_235,plain,
m_NormQ(X1) != m_NotNorm(X2),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_236,plain,
m_NormQ(X1) != m_Halt(X2),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_237,plain,
m_Ldr(X1) != m_NormQ(X2),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_238,plain,
m_Down(X1) != m_NormQ(X2),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_239,plain,
m_Ldr(X1) != m_NotNorm(X2),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_240,plain,
m_Ldr(X1) != m_Halt(X2),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_241,plain,
m_Down(X1) != m_Ldr(X2),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_242,plain,
m_NotNorm(X1) != m_Halt(X2),
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_243,plain,
m_Down(X1) != m_NotNorm(X2),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_244,plain,
m_Down(X1) != m_Halt(X2),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_245,plain,
( pidElem(X1)
| X1 != m_Down(X2) ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_246,plain,
( pidElem(X1)
| X1 != m_Halt(X2) ),
inference(split_conjunct,[status(thm)],[i_0_95]),
[final] ).
cnf(i_0_247,negated_conjecture,
setIn(esk13_0,alive),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_248,negated_conjecture,
setIn(esk10_0,alive),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_249,negated_conjecture,
setIn(esk7_0,alive),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_250,plain,
pidMsg(m_Down(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_251,plain,
pidMsg(m_Halt(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_252,negated_conjecture,
host(esk11_0) = s(host(esk13_0)),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_253,negated_conjecture,
host(esk7_0) != host(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_254,negated_conjecture,
host(esk9_0) = host(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_255,negated_conjecture,
host(esk7_0) = host(esk10_0),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_256,negated_conjecture,
host(esk7_0) = host(esk10_0),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_257,plain,
ordered(q_nil),
inference(split_conjunct,[status(thm)],[axiom_51]),
[final] ).
cnf(i_0_258,plain,
norm != wait,
inference(split_conjunct,[status(thm)],[axiom_10]),
[final] ).
cnf(i_0_259,plain,
elec_2 != norm,
inference(split_conjunct,[status(thm)],[axiom_09]),
[final] ).
cnf(i_0_260,plain,
elec_1 != norm,
inference(split_conjunct,[status(thm)],[axiom_07]),
[final] ).
cnf(i_0_261,plain,
elec_2 != wait,
inference(split_conjunct,[status(thm)],[axiom_08]),
[final] ).
cnf(i_0_262,plain,
elec_1 != wait,
inference(split_conjunct,[status(thm)],[axiom_06]),
[final] ).
cnf(i_0_263,plain,
elec_1 != elec_2,
inference(split_conjunct,[status(thm)],[axiom_05]),
[final] ).
cnf(i_0_264,axiom,
X1 = X1 ).
cnf(i_0_265,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_266,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_267,axiom,
( X1 != X2
| esk15_8(X1,X3,X4,X5,X6,X7,X8,X9) = esk15_8(X2,X3,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_268,axiom,
( X1 != X2
| esk15_8(X3,X1,X4,X5,X6,X7,X8,X9) = esk15_8(X3,X2,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_269,axiom,
( X1 != X2
| esk15_8(X3,X4,X1,X5,X6,X7,X8,X9) = esk15_8(X3,X4,X2,X5,X6,X7,X8,X9) ) ).
cnf(i_0_270,axiom,
( X1 != X2
| esk15_8(X3,X4,X5,X1,X6,X7,X8,X9) = esk15_8(X3,X4,X5,X2,X6,X7,X8,X9) ) ).
cnf(i_0_271,axiom,
( X1 != X2
| esk15_8(X3,X4,X5,X6,X1,X7,X8,X9) = esk15_8(X3,X4,X5,X6,X2,X7,X8,X9) ) ).
cnf(i_0_272,axiom,
( X1 != X2
| esk15_8(X3,X4,X5,X6,X7,X1,X8,X9) = esk15_8(X3,X4,X5,X6,X7,X2,X8,X9) ) ).
cnf(i_0_273,axiom,
( X1 != X2
| esk15_8(X3,X4,X5,X6,X7,X8,X1,X9) = esk15_8(X3,X4,X5,X6,X7,X8,X2,X9) ) ).
cnf(i_0_274,axiom,
( X1 != X2
| esk15_8(X3,X4,X5,X6,X7,X8,X9,X1) = esk15_8(X3,X4,X5,X6,X7,X8,X9,X2) ) ).
cnf(i_0_275,axiom,
( X1 != X2
| cons(X1,X3) = cons(X2,X3) ) ).
cnf(i_0_276,axiom,
( X1 != X2
| cons(X3,X1) = cons(X3,X2) ) ).
cnf(i_0_277,axiom,
( X1 != X2
| snoc(X1,X3) = snoc(X2,X3) ) ).
cnf(i_0_278,axiom,
( X1 != X2
| snoc(X3,X1) = snoc(X3,X2) ) ).
cnf(i_0_279,axiom,
( X1 != X2
| pidMsg(X1) = pidMsg(X2) ) ).
cnf(i_0_280,axiom,
( X1 != X2
| m_Halt(X1) = m_Halt(X2) ) ).
cnf(i_0_281,axiom,
( X1 != X2
| init(X1) = init(X2) ) ).
cnf(i_0_282,axiom,
( X1 != X2
| last(X1) = last(X2) ) ).
cnf(i_0_283,axiom,
( X1 != X2
| tail(X1) = tail(X2) ) ).
cnf(i_0_284,axiom,
( X1 != X2
| head(X1) = head(X2) ) ).
cnf(i_0_285,axiom,
( X1 != X2
| index(X1,X3) = index(X2,X3) ) ).
cnf(i_0_286,axiom,
( X1 != X2
| index(X3,X1) = index(X3,X2) ) ).
cnf(i_0_287,axiom,
( X1 != X2
| m_NormQ(X1) = m_NormQ(X2) ) ).
cnf(i_0_288,axiom,
( X1 != X2
| m_NotNorm(X1) = m_NotNorm(X2) ) ).
cnf(i_0_289,axiom,
( X1 != X2
| host(X1) = host(X2) ) ).
cnf(i_0_290,axiom,
( X1 != X2
| s(X1) = s(X2) ) ).
cnf(i_0_291,axiom,
( X1 != X2
| m_Down(X1) = m_Down(X2) ) ).
cnf(i_0_292,axiom,
( X1 != X2
| queue(X1) = queue(X2) ) ).
cnf(i_0_293,axiom,
( X1 != X2
| esk14_8(X1,X3,X4,X5,X6,X7,X8,X9) = esk14_8(X2,X3,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_294,axiom,
( X1 != X2
| esk14_8(X3,X1,X4,X5,X6,X7,X8,X9) = esk14_8(X3,X2,X4,X5,X6,X7,X8,X9) ) ).
cnf(i_0_295,axiom,
( X1 != X2
| esk14_8(X3,X4,X1,X5,X6,X7,X8,X9) = esk14_8(X3,X4,X2,X5,X6,X7,X8,X9) ) ).
cnf(i_0_296,axiom,
( X1 != X2
| esk14_8(X3,X4,X5,X1,X6,X7,X8,X9) = esk14_8(X3,X4,X5,X2,X6,X7,X8,X9) ) ).
cnf(i_0_297,axiom,
( X1 != X2
| esk14_8(X3,X4,X5,X6,X1,X7,X8,X9) = esk14_8(X3,X4,X5,X6,X2,X7,X8,X9) ) ).
cnf(i_0_298,axiom,
( X1 != X2
| esk14_8(X3,X4,X5,X6,X7,X1,X8,X9) = esk14_8(X3,X4,X5,X6,X7,X2,X8,X9) ) ).
cnf(i_0_299,axiom,
( X1 != X2
| esk14_8(X3,X4,X5,X6,X7,X8,X1,X9) = esk14_8(X3,X4,X5,X6,X7,X8,X2,X9) ) ).
cnf(i_0_300,axiom,
( X1 != X2
| esk14_8(X3,X4,X5,X6,X7,X8,X9,X1) = esk14_8(X3,X4,X5,X6,X7,X8,X9,X2) ) ).
cnf(i_0_301,axiom,
( X1 != X2
| m_Ack(X1,X3) = m_Ack(X2,X3) ) ).
cnf(i_0_302,axiom,
( X1 != X2
| m_Ack(X3,X1) = m_Ack(X3,X2) ) ).
cnf(i_0_303,axiom,
( X1 != X2
| m_Ldr(X1) = m_Ldr(X2) ) ).
cnf(i_0_304,axiom,
( X1 != X2
| ~ setIn(X1,X3)
| setIn(X2,X3) ) ).
cnf(i_0_305,axiom,
( X1 != X2
| ~ setIn(X3,X1)
| setIn(X3,X2) ) ).
cnf(i_0_306,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_307,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_308,axiom,
( X1 != X2
| ~ elem(X1,X3)
| elem(X2,X3) ) ).
cnf(i_0_309,axiom,
( X1 != X2
| ~ elem(X3,X1)
| elem(X3,X2) ) ).
cnf(i_0_310,axiom,
( X1 != X2
| ~ epred1_4(X1,X3,X4,X5)
| epred1_4(X2,X3,X4,X5) ) ).
cnf(i_0_311,axiom,
( X1 != X2
| ~ epred1_4(X3,X1,X4,X5)
| epred1_4(X3,X2,X4,X5) ) ).
cnf(i_0_312,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X1,X5)
| epred1_4(X3,X4,X2,X5) ) ).
cnf(i_0_313,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X5,X1)
| epred1_4(X3,X4,X5,X2) ) ).
cnf(i_0_314,axiom,
( X1 != X2
| ~ ordered(X1)
| ordered(X2) ) ).
cnf(i_0_315,axiom,
( X1 != X2
| ~ pidElem(X1)
| pidElem(X2) ) ).
cnf(i_0_321,plain,
X1 = X1,
inference(equality_inference,[],[187]) ).
cnf(i_0_322,plain,
X1 = X1,
inference(equality_inference,[],[188]) ).
cnf(i_0_323,plain,
elem(X1,snoc(X2,X1)),
inference(equality_inference,[],[189]) ).
cnf(i_0_324,plain,
elem(X1,cons(X1,X2)),
inference(equality_inference,[],[190]) ).
cnf(i_0_325,plain,
leq(X1,X1),
inference(equality_inference,[],[222]) ).
cnf(i_0_326,plain,
leq(X1,X1),
inference(equality_inference,[],[223]) ).
cnf(i_0_327,plain,
X1 = X1,
inference(equality_inference,[],[229]) ).
cnf(i_0_328,plain,
X1 = X1,
inference(equality_inference,[],[230]) ).
cnf(i_0_329,plain,
X1 = X1,
inference(equality_inference,[],[231]) ).
cnf(i_0_330,plain,
X1 = X1,
inference(equality_inference,[],[232]) ).
cnf(i_0_331,plain,
X1 = X1,
inference(equality_inference,[],[233]) ).
cnf(i_0_332,plain,
pidElem(m_Down(X1)),
inference(equality_inference,[],[245]) ).
cnf(i_0_333,plain,
pidElem(m_Halt(X1)),
inference(equality_inference,[],[246]) ).
cnf(i_0_349,plain,
~ leq(s(s(X1)),X1),
inference(scs_inference,[],[i_0_196,i_0_191]) ).
cnf(i_0_350,plain,
~ leq(s(X1),X1),
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_352,plain,
leq(host(esk9_0),host(esk13_0)),
inference(scs_inference,[],[i_0_254,i_0_196,i_0_191,i_0_222]) ).
cnf(i_0_354,plain,
leq(host(esk13_0),host(esk9_0)),
inference(scs_inference,[],[i_0_254,i_0_196,i_0_191,i_0_222,i_0_223]) ).
cnf(i_0_363,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_366,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_369,plain,
~ leq(s(X1),X1),
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_377,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_379,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_381,plain,
~ leq(s(X1),X1),
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_383,plain,
~ leq(s(X1),X1),
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_385,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_387,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_389,plain,
m_Down(X1) != m_Ldr(X2),
inference(rename_variables,[],[i_0_241]) ).
cnf(i_0_392,plain,
m_Ack(X1,X2) != m_Down(X3),
inference(rename_variables,[],[i_0_209]) ).
cnf(i_0_393,plain,
m_Ack(X1,X2) != m_Halt(X3),
inference(rename_variables,[],[i_0_210]) ).
cnf(i_0_403,plain,
ordered(snoc(q_nil,X1)),
inference(rename_variables,[],[i_0_211]) ).
cnf(i_0_408,plain,
leq(host(esk7_0),host(esk10_0)),
inference(scs_inference,[],[i_0_256,i_0_222]) ).
cnf(i_0_410,plain,
leq(host(esk10_0),host(esk7_0)),
inference(scs_inference,[],[i_0_256,i_0_222,i_0_223]) ).
cnf(i_0_417,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_420,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_431,plain,
m_Down(X1) != m_Ldr(X2),
inference(rename_variables,[],[i_0_241]) ).
cnf(i_0_434,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_436,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_438,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_443,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_445,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_453,plain,
ordered(cons(X1,q_nil)),
inference(rename_variables,[],[i_0_212]) ).
cnf(i_0_456,plain,
leq(index(status,host(esk13_0)),elec_1),
inference(scs_inference,[],[i_0_227,i_0_222]) ).
cnf(i_0_458,plain,
leq(elec_1,index(status,host(esk13_0))),
inference(scs_inference,[],[i_0_227,i_0_222,i_0_223]) ).
cnf(i_0_463,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_466,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_476,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_478,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_480,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_484,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_486,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_492,plain,
ordered(cons(X1,q_nil)),
inference(rename_variables,[],[i_0_212]) ).
cnf(i_0_494,plain,
leq(index(status,host(esk7_0)),elec_2),
inference(scs_inference,[],[i_0_228,i_0_222]) ).
cnf(i_0_496,plain,
leq(elec_2,index(status,host(esk7_0))),
inference(scs_inference,[],[i_0_228,i_0_222,i_0_223]) ).
cnf(i_0_498,plain,
pidElem(last(snoc(X1,m_Down(X2)))),
inference(scs_inference,[],[i_0_228,i_0_198,i_0_222,i_0_223,i_0_245]) ).
cnf(i_0_499,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_502,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_513,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_515,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_517,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_519,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_523,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_525,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_531,plain,
ordered(cons(X1,q_nil)),
inference(rename_variables,[],[i_0_212]) ).
cnf(i_0_533,plain,
pidElem(tail(cons(X1,m_Down(X2)))),
inference(scs_inference,[],[i_0_199,i_0_245]) ).
cnf(i_0_534,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_537,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_550,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_552,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_554,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_557,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_559,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_561,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_568,plain,
pidElem(head(cons(m_Down(X1),X2))),
inference(scs_inference,[],[i_0_200,i_0_245]) ).
cnf(i_0_569,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_572,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_585,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_587,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_589,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_591,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_593,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_595,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_601,plain,
leq(host(esk11_0),s(host(esk13_0))),
inference(scs_inference,[],[i_0_252,i_0_222]) ).
cnf(i_0_603,plain,
leq(s(host(esk13_0)),host(esk11_0)),
inference(scs_inference,[],[i_0_252,i_0_222,i_0_223]) ).
cnf(i_0_612,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_614,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_616,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_620,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_626,plain,
ordered(cons(X1,q_nil)),
inference(rename_variables,[],[i_0_212]) ).
cnf(i_0_639,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_641,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_658,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_660,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_677,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_679,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_699,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_701,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_718,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_720,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_737,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_739,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_761,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_763,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_766,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_787,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_789,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_791,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_794,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_815,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_817,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_820,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_844,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_846,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_848,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_850,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_869,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_871,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_873,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_875,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_890,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_892,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_894,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_896,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_920,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_922,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_924,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_950,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_952,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_954,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_956,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_969,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_973,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_975,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_977,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_989,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_991,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_993,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_995,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_997,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1016,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1021,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1023,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1027,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1041,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1047,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1050,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1064,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1066,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1069,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1071,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1073,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1084,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1086,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1089,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1091,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1093,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1110,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1112,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1114,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1119,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1129,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1131,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1133,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1135,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1137,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1147,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1149,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1151,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1153,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1164,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1166,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1168,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1174,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1176,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1178,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1180,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1188,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1190,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_1196,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1200,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1206,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1208,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1214,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1216,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1222,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1224,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1233,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1235,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1241,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1243,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1249,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1251,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1257,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1263,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1270,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1276,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1282,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1288,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1294,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1300,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1306,plain,
~ leq(s(X1),X1),
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_1308,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1314,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1321,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1328,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1345,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1362,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1370,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1377,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1384,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1391,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1397,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1403,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1405,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1411,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1417,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1608,plain,
pidMsg(m_Halt(X1)) = X1,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_1614,plain,
init(snoc(X1,X2)) = X1,
inference(rename_variables,[],[i_0_197]) ).
cnf(i_0_1620,plain,
last(snoc(X1,X2)) = X2,
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_1626,plain,
tail(cons(X1,X2)) = X2,
inference(rename_variables,[],[i_0_199]) ).
cnf(i_0_1632,plain,
head(cons(X1,X2)) = X1,
inference(rename_variables,[],[i_0_200]) ).
cnf(i_0_1803,plain,
m_Down(X1) != m_Halt(X2),
inference(rename_variables,[],[i_0_244]) ).
cnf(i_0_1814,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_1998,plain,
leq(X1,X1),
inference(rename_variables,[],[i_0_234]) ).
cnf(i_0_2079,plain,
snoc(cons(X1,X2),X3) = cons(X1,snoc(X2,X3)),
inference(rename_variables,[],[i_0_169]) ).
cnf(i_0_2100,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_2214,plain,
~ leq(s(X1),X1),
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_2356,plain,
m_NormQ(X1) != m_Halt(X2),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_2447,plain,
m_Ldr(X1) != m_NotNorm(X2),
inference(rename_variables,[],[i_0_239]) ).
cnf(i_0_2460,plain,
m_Ldr(X1) != m_NotNorm(X2),
inference(rename_variables,[],[i_0_239]) ).
cnf(i_0_2692,plain,
m_Ldr(X1) != m_Halt(X2),
inference(rename_variables,[],[i_0_240]) ).
cnf(i_0_2697,plain,
m_Ldr(X1) != m_Halt(X2),
inference(rename_variables,[],[i_0_240]) ).
cnf(i_0_3049,plain,
pidMsg(m_Down(X1)) = X1,
inference(rename_variables,[],[i_0_250]) ).
cnf(i_0_348,plain,
~ elem(m_Down(X1),queue(host(X1))),
inference(scs_inference,[],[i_0_155,i_0_316]) ).
cnf(i_0_356,plain,
~ elem(m_Down(esk9_0),queue(host(esk13_0))),
inference(scs_inference,[],[i_0_254,i_0_196,i_0_191,i_0_222,i_0_223,i_0_344]) ).
cnf(i_0_358,plain,
host(esk13_0) = host(esk9_0),
inference(scs_inference,[],[i_0_254,i_0_196,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265]) ).
cnf(i_0_359,plain,
esk7_0 != esk13_0,
inference(scs_inference,[],[i_0_253,i_0_254,i_0_196,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289]) ).
cnf(i_0_360,plain,
leq(X1,s(X1)),
inference(scs_inference,[],[i_0_253,i_0_254,i_0_196,i_0_350,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203]) ).
cnf(i_0_362,plain,
pidElem(pidMsg(m_Down(m_Down(X1)))),
inference(scs_inference,[],[i_0_253,i_0_254,i_0_196,i_0_350,i_0_250,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245]) ).
cnf(i_0_365,plain,
pidElem(pidMsg(m_Down(m_Halt(X1)))),
inference(scs_inference,[],[i_0_253,i_0_254,i_0_196,i_0_350,i_0_250,i_0_363,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246]) ).
cnf(i_0_368,plain,
~ leq(s(s(host(esk13_0))),nbr_proc),
inference(scs_inference,[],[i_0_253,i_0_254,i_0_213,i_0_196,i_0_350,i_0_250,i_0_363,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178]) ).
cnf(i_0_371,plain,
index(elid,host(esk7_0)) = esk7_0,
inference(scs_inference,[],[i_0_249,i_0_253,i_0_254,i_0_213,i_0_228,i_0_196,i_0_350,i_0_250,i_0_363,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345]) ).
cnf(i_0_373,plain,
index(elid,host(esk13_0)) = esk13_0,
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_213,i_0_227,i_0_228,i_0_196,i_0_350,i_0_250,i_0_363,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346]) ).
cnf(i_0_375,plain,
host(esk7_0) != host(esk9_0),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_213,i_0_227,i_0_228,i_0_196,i_0_350,i_0_250,i_0_363,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266]) ).
cnf(i_0_376,plain,
~ setIn(pidMsg(m_Down(nil)),alive),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_213,i_0_227,i_0_228,i_0_196,i_0_350,i_0_224,i_0_250,i_0_363,i_0_366,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304]) ).
cnf(i_0_378,plain,
~ setIn(X1,pidMsg(m_Down(setEmpty))),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_213,i_0_227,i_0_228,i_0_218,i_0_196,i_0_350,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305]) ).
cnf(i_0_380,plain,
~ leq(host(esk11_0),host(esk13_0)),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_252,i_0_213,i_0_227,i_0_228,i_0_218,i_0_196,i_0_350,i_0_369,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305,i_0_306]) ).
cnf(i_0_382,plain,
~ leq(s(host(esk13_0)),host(esk9_0)),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_252,i_0_213,i_0_227,i_0_228,i_0_218,i_0_196,i_0_350,i_0_369,i_0_381,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305,i_0_306,i_0_307]) ).
cnf(i_0_384,plain,
~ elem(pidMsg(m_Down(m_Down(esk9_0))),queue(host(esk13_0))),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_252,i_0_213,i_0_227,i_0_228,i_0_218,i_0_196,i_0_350,i_0_369,i_0_381,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_379,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308]) ).
cnf(i_0_386,plain,
~ elem(X1,pidMsg(m_Down(q_nil))),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_252,i_0_213,i_0_227,i_0_228,i_0_218,i_0_219,i_0_196,i_0_350,i_0_369,i_0_381,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_379,i_0_385,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309]) ).
cnf(i_0_388,plain,
elem(m_Down(esk11_0),queue(host(esk13_0))),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_173,i_0_252,i_0_213,i_0_227,i_0_228,i_0_218,i_0_219,i_0_196,i_0_350,i_0_369,i_0_381,i_0_241,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_379,i_0_385,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_168]) ).
cnf(i_0_391,plain,
~ pidElem(m_Ack(X1,X2)),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_173,i_0_252,i_0_213,i_0_227,i_0_228,i_0_218,i_0_219,i_0_196,i_0_350,i_0_369,i_0_381,i_0_209,i_0_210,i_0_241,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_379,i_0_385,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_168,i_0_201]) ).
cnf(i_0_397,plain,
m_Down(X1) != m_Ack(X2,X3),
inference(scs_inference,[],[i_0_247,i_0_249,i_0_253,i_0_254,i_0_173,i_0_252,i_0_213,i_0_227,i_0_228,i_0_332,i_0_218,i_0_219,i_0_196,i_0_350,i_0_369,i_0_381,i_0_209,i_0_210,i_0_241,i_0_224,i_0_250,i_0_363,i_0_366,i_0_377,i_0_379,i_0_385,i_0_191,i_0_222,i_0_223,i_0_344,i_0_265,i_0_289,i_0_203,i_0_245,i_0_246,i_0_178,i_0_345,i_0_346,i_0_266,i_0_304,i_0_305,i_0_306,i_0_307,i_0_308,i_0_309,i_0_168,i_0_201,i_0_186,i_0_315]) ).
cnf(i_0_405,plain,
~ elem(m_Down(X1),queue(host(X1))),
inference(equality_inference,[],[344]) ).
cnf(i_0_412,plain,
~ elem(m_Down(esk7_0),queue(host(esk10_0))),
inference(scs_inference,[],[i_0_256,i_0_222,i_0_223,i_0_344]) ).
cnf(i_0_414,plain,
leq(X1,s(s(X1))),
inference(scs_inference,[],[i_0_256,i_0_349,i_0_222,i_0_223,i_0_344,i_0_203]) ).
cnf(i_0_416,plain,
pidElem(pidMsg(m_Halt(m_Down(X1)))),
inference(scs_inference,[],[i_0_256,i_0_349,i_0_251,i_0_222,i_0_223,i_0_344,i_0_203,i_0_245]) ).
cnf(i_0_419,plain,
pidElem(pidMsg(m_Halt(m_Halt(X1)))),
inference(scs_inference,[],[i_0_256,i_0_349,i_0_251,i_0_417,i_0_222,i_0_223,i_0_344,i_0_203,i_0_245,i_0_246]) ).
cnf(i_0_422,plain,
~ leq(s(s(s(X1))),X1),
inference(scs_inference,[],[i_0_256,i_0_349,i_0_251,i_0_417,i_0_222,i_0_223,i_0_344,i_0_203,i_0_245,i_0_246,i_0_191]) ).
cnf(i_0_423,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_425,plain,
host(esk10_0) = host(esk7_0),
inference(scs_inference,[],[i_0_256,i_0_349,i_0_251,i_0_417,i_0_222,i_0_223,i_0_344,i_0_203,i_0_245,i_0_246,i_0_191,i_0_265]) ).
cnf(i_0_428,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_441,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_451,plain,
elem(X1,snoc(X2,X1)),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_501,plain,
pidElem(last(snoc(X1,m_Halt(X2)))),
inference(scs_inference,[],[i_0_228,i_0_198,i_0_499,i_0_222,i_0_223,i_0_245,i_0_246]) ).
cnf(i_0_510,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_521,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_536,plain,
pidElem(tail(cons(X1,m_Halt(X2)))),
inference(scs_inference,[],[i_0_199,i_0_534,i_0_245,i_0_246]) ).
cnf(i_0_539,plain,
leq(index(elid,host(esk7_0)),esk6_0),
inference(scs_inference,[],[i_0_226,i_0_199,i_0_534,i_0_245,i_0_246,i_0_222]) ).
cnf(i_0_541,plain,
leq(esk6_0,index(elid,host(esk7_0))),
inference(scs_inference,[],[i_0_226,i_0_199,i_0_534,i_0_245,i_0_246,i_0_222,i_0_223]) ).
cnf(i_0_547,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_571,plain,
pidElem(head(cons(m_Halt(X1),X2))),
inference(scs_inference,[],[i_0_200,i_0_569,i_0_245,i_0_246]) ).
cnf(i_0_574,plain,
leq(host(esk8_0),index(pendack,host(esk7_0))),
inference(scs_inference,[],[i_0_221,i_0_200,i_0_569,i_0_245,i_0_246,i_0_222]) ).
cnf(i_0_576,plain,
leq(index(pendack,host(esk7_0)),host(esk8_0)),
inference(scs_inference,[],[i_0_221,i_0_200,i_0_569,i_0_245,i_0_246,i_0_222,i_0_223]) ).
cnf(i_0_597,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_636,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_655,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_674,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_696,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_715,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_734,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_758,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_783,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_819,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_863,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_1038,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_1061,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_1230,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_1506,plain,
~ leq(s(s(X1)),X1),
inference(rename_variables,[],[i_0_349]) ).
cnf(c_0_412,plain,
( X1 = X2
| elem(X1,X3)
| ~ elem(X1,snoc(X3,X2)) ),
i_0_168 ).
cnf(c_0_413,negated_conjecture,
elem(m_Down(esk12_0),snoc(queue(host(esk13_0)),m_Ldr(esk7_0))),
i_0_172 ).
cnf(c_0_414,plain,
m_Down(X1) != m_Ldr(X2),
i_0_241 ).
cnf(c_0_415,negated_conjecture,
leq(nbr_proc,s(host(esk13_0))),
i_0_213 ).
cnf(c_0_416,negated_conjecture,
host(esk11_0) = s(host(esk13_0)),
i_0_252 ).
cnf(c_0_417,negated_conjecture,
( leq(host(esk13_0),X1)
| setIn(X1,index(down,host(esk13_0)))
| X1 = host(esk12_0)
| ~ leq(s(zero),X1) ),
i_0_165 ).
cnf(c_0_418,plain,
leq(s(zero),host(X1)),
i_0_215 ).
cnf(c_0_419,plain,
( leq(index(pendack,host(X1)),host(X2))
| ~ setIn(X2,alive)
| ~ setIn(X1,alive)
| ~ elem(m_Down(X3),queue(host(X2)))
| host(X1) != host(X3)
| index(status,host(X1)) != elec_2
| ~ epred1_4(X4,X5,X6,X7) ),
i_0_144 ).
cnf(c_0_420,negated_conjecture,
elem(m_Down(esk12_0),queue(host(esk13_0))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_412,c_0_413]),c_0_414]) ).
cnf(c_0_421,negated_conjecture,
setIn(esk13_0,alive),
i_0_247 ).
cnf(c_0_422,negated_conjecture,
leq(nbr_proc,index(pendack,host(esk7_0))),
i_0_194 ).
cnf(c_0_423,negated_conjecture,
host(esk8_0) = index(pendack,host(esk7_0)),
i_0_221 ).
cnf(c_0_424,plain,
( X1 = X2
| ~ leq(X1,X2)
| ~ leq(X2,X1) ),
i_0_186 ).
cnf(c_0_425,negated_conjecture,
leq(nbr_proc,host(esk11_0)),
inference(rw,[status(thm)],[c_0_415,c_0_416]) ).
cnf(c_0_426,plain,
leq(host(X1),nbr_proc),
i_0_220 ).
cnf(c_0_427,plain,
( leq(index(pendack,host(X1)),host(X2))
| ~ setIn(X2,alive)
| ~ setIn(X1,alive)
| ~ setIn(host(X1),index(down,host(X2)))
| index(status,host(X1)) != elec_2
| ~ epred1_4(X3,X4,X5,X6) ),
i_0_142 ).
cnf(c_0_428,plain,
( host(X1) = host(esk12_0)
| leq(host(esk13_0),host(X1))
| setIn(host(X1),index(down,host(esk13_0))) ),
inference(spm,[status(thm)],[c_0_417,c_0_418]) ).
cnf(c_0_429,negated_conjecture,
( leq(index(pendack,host(X1)),host(esk13_0))
| index(status,host(X1)) != elec_2
| host(X1) != host(esk12_0)
| ~ epred1_4(X2,X3,X4,X5)
| ~ setIn(X1,alive) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_419,c_0_420]),c_0_421])]) ).
cnf(c_0_430,negated_conjecture,
leq(nbr_proc,host(esk8_0)),
inference(rw,[status(thm)],[c_0_422,c_0_423]) ).
cnf(c_0_431,plain,
~ leq(host(esk11_0),host(esk13_0)),
i_0_380 ).
cnf(c_0_432,negated_conjecture,
host(esk11_0) = nbr_proc,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_424,c_0_425]),c_0_426])]) ).
cnf(c_0_433,negated_conjecture,
index(elid,host(esk7_0)) = esk6_0,
i_0_226 ).
cnf(c_0_434,plain,
index(elid,host(esk7_0)) = esk7_0,
i_0_371 ).
cnf(c_0_435,plain,
( leq(index(pendack,host(X1)),host(esk13_0))
| leq(host(esk13_0),host(X1))
| index(status,host(X1)) != elec_2
| ~ epred1_4(X2,X3,X4,X5)
| ~ setIn(X1,alive) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_427,c_0_428]),c_0_421])]),c_0_429]) ).
cnf(c_0_436,negated_conjecture,
index(status,host(esk7_0)) = elec_2,
i_0_228 ).
cnf(c_0_437,negated_conjecture,
host(esk8_0) = nbr_proc,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_424,c_0_430]),c_0_426])]) ).
cnf(c_0_438,negated_conjecture,
setIn(esk7_0,alive),
i_0_249 ).
cnf(c_0_439,plain,
~ leq(nbr_proc,host(esk13_0)),
inference(rw,[status(thm)],[c_0_431,c_0_432]) ).
cnf(c_0_440,negated_conjecture,
epred1_4(esk5_0,esk8_0,esk7_0,esk6_0),
i_0_155 ).
cnf(c_0_441,negated_conjecture,
esk6_0 = esk7_0,
inference(rw,[status(thm)],[c_0_433,c_0_434]) ).
cnf(c_0_442,negated_conjecture,
( leq(host(esk13_0),host(esk7_0))
| ~ epred1_4(X1,X2,X3,X4) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_435,c_0_436]),c_0_423]),c_0_437]),c_0_438])]),c_0_439]) ).
cnf(c_0_443,negated_conjecture,
epred1_4(esk5_0,esk8_0,esk7_0,esk7_0),
inference(rw,[status(thm)],[c_0_440,c_0_441]) ).
cnf(c_0_444,plain,
( X1 = s(X2)
| leq(X1,X2)
| ~ leq(X1,s(X2)) ),
i_0_182 ).
cnf(c_0_445,negated_conjecture,
s(host(esk13_0)) = nbr_proc,
inference(rw,[status(thm)],[c_0_416,c_0_432]) ).
cnf(c_0_446,plain,
elem(m_Down(esk11_0),queue(host(esk13_0))),
i_0_388 ).
cnf(c_0_447,negated_conjecture,
leq(host(esk13_0),host(esk7_0)),
inference(spm,[status(thm)],[c_0_442,c_0_443]) ).
cnf(c_0_448,negated_conjecture,
host(esk7_0) != host(esk13_0),
i_0_253 ).
cnf(c_0_449,negated_conjecture,
( X1 = nbr_proc
| leq(X1,host(esk13_0))
| ~ leq(X1,nbr_proc) ),
inference(spm,[status(thm)],[c_0_444,c_0_445]) ).
cnf(c_0_450,plain,
( leq(index(pendack,host(X1)),host(esk13_0))
| index(status,host(X1)) != elec_2
| host(X1) != nbr_proc
| ~ epred1_4(X2,X3,X4,X5)
| ~ setIn(X1,alive) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_419,c_0_446]),c_0_432]),c_0_421])]) ).
cnf(c_0_451,plain,
~ leq(host(esk7_0),host(esk13_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_424,c_0_447]),c_0_448]) ).
cnf(c_0_452,plain,
( host(X1) = nbr_proc
| leq(host(X1),host(esk13_0)) ),
inference(spm,[status(thm)],[c_0_449,c_0_426]) ).
cnf(c_0_453,negated_conjecture,
( host(esk7_0) != nbr_proc
| ~ epred1_4(X1,X2,X3,X4) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_450,c_0_436]),c_0_423]),c_0_437]),c_0_438])]),c_0_439]) ).
cnf(c_0_454,plain,
host(esk7_0) = nbr_proc,
inference(spm,[status(thm)],[c_0_451,c_0_452]) ).
cnf(c_0_455,negated_conjecture,
~ epred1_4(X1,X2,X3,X4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_453,c_0_454])]) ).
cnf(c_0_456,negated_conjecture,
$false,
inference(sr,[status(thm)],[c_0_443,c_0_455]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWV475+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n009.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 05:17:56 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 232.32/145.70 % Version : CSE_E---1.7
% 232.32/145.70 % Problem : theBenchmark.p
% 232.32/145.70 % SZS status Theorem for theBenchmark.p
% 232.32/145.70 % SZS output start CNFRefutation
% See solution above
% 245.91/159.36 % Total time : 144.561s
%------------------------------------------------------------------------------