%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWV463+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:03:45 AM UTC 2026
% Result : Theorem 11.05s 16.33s
% Output : Proof 11.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(axiom,axiom,
! [Pid,Pid2] :
( elem(m_Ack(Pid,Pid2),queue(host(Pid)))
=> ( setIn(Pid2,pids)
& setIn(Pid,pids) ) ),
file('SWV011+0.ax',axiom) ).
fof(axiom_01,axiom,
! [P,Q] :
( s(host(P)) = host(Q)
=> host(P) != host(Q) ),
file('SWV011+0.ax',axiom_01) ).
fof(axiom_02,axiom,
! [P] : leq(s(zero),host(P)),
file('SWV011+0.ax',axiom_02) ).
fof(axiom_03,axiom,
leq(s(zero),nbr_proc),
file('SWV011+0.ax',axiom_03) ).
fof(axiom_04,axiom,
! [P] : leq(host(P),nbr_proc),
file('SWV011+0.ax',axiom_04) ).
fof(axiom_05,axiom,
elec_1 != elec_2,
file('SWV011+0.ax',axiom_05) ).
fof(axiom_06,axiom,
elec_1 != wait,
file('SWV011+0.ax',axiom_06) ).
fof(axiom_07,axiom,
elec_1 != norm,
file('SWV011+0.ax',axiom_07) ).
fof(axiom_08,axiom,
elec_2 != wait,
file('SWV011+0.ax',axiom_08) ).
fof(axiom_09,axiom,
elec_2 != norm,
file('SWV011+0.ax',axiom_09) ).
fof(axiom_10,axiom,
norm != wait,
file('SWV011+0.ax',axiom_10) ).
fof(axiom_11,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z),
file('SWV011+0.ax',axiom_11) ).
fof(axiom_12,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z),
file('SWV011+0.ax',axiom_12) ).
fof(axiom_13,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_NotNorm(Z),
file('SWV011+0.ax',axiom_13) ).
fof(axiom_14,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z),
file('SWV011+0.ax',axiom_14) ).
fof(axiom_15,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z),
file('SWV011+0.ax',axiom_15) ).
fof(axiom_16,axiom,
! [X,Y] : m_NotNorm(X) != m_Halt(Y),
file('SWV011+0.ax',axiom_16) ).
fof(axiom_17,axiom,
! [X,Y] : m_Down(X) != m_Halt(Y),
file('SWV011+0.ax',axiom_17) ).
fof(axiom_18,axiom,
! [X,Y] : m_Down(X) != m_Ldr(Y),
file('SWV011+0.ax',axiom_18) ).
fof(axiom_19,axiom,
! [X,Y] : m_Down(X) != m_NotNorm(Y),
file('SWV011+0.ax',axiom_19) ).
fof(axiom_20,axiom,
! [X,Y] : m_Down(X) != m_NormQ(Y),
file('SWV011+0.ax',axiom_20) ).
fof(axiom_21,axiom,
! [X,Y] : m_NormQ(X) != m_Halt(Y),
file('SWV011+0.ax',axiom_21) ).
fof(axiom_22,axiom,
! [X,Y] : m_Ldr(X) != m_Halt(Y),
file('SWV011+0.ax',axiom_22) ).
fof(axiom_23,axiom,
! [X,Y] : m_Ldr(X) != m_NormQ(Y),
file('SWV011+0.ax',axiom_23) ).
fof(axiom_24,axiom,
! [X,Y] : m_Ldr(X) != m_NotNorm(Y),
file('SWV011+0.ax',axiom_24) ).
fof(axiom_25,axiom,
! [X,Y] : m_NormQ(X) != m_NotNorm(Y),
file('SWV011+0.ax',axiom_25) ).
fof(axiom_26,axiom,
! [X,Y] :
( X != Y
<=> m_Halt(X) != m_Halt(Y) ),
file('SWV011+0.ax',axiom_26) ).
fof(axiom_27,axiom,
! [X,Y] :
( X != Y
<=> m_NormQ(X) != m_NormQ(Y) ),
file('SWV011+0.ax',axiom_27) ).
fof(axiom_28,axiom,
! [X,Y] :
( X != Y
<=> m_NotNorm(X) != m_NotNorm(Y) ),
file('SWV011+0.ax',axiom_28) ).
fof(axiom_29,axiom,
! [X,Y] :
( X != Y
<=> m_Ldr(X) != m_Ldr(Y) ),
file('SWV011+0.ax',axiom_29) ).
fof(axiom_30,axiom,
! [X,Y] :
( X != Y
<=> m_Down(X) != m_Down(Y) ),
file('SWV011+0.ax',axiom_30) ).
fof(axiom_31,axiom,
! [X1,X2,Y1,Y2] :
( X1 != X2
=> m_Ack(X1,Y1) != m_Ack(X2,Y2) ),
file('SWV011+0.ax',axiom_31) ).
fof(axiom_32,axiom,
! [X1,X2,Y1,Y2] :
( Y1 != Y2
=> m_Ack(X1,Y1) != m_Ack(X2,Y2) ),
file('SWV011+0.ax',axiom_32) ).
fof(axiom_33,axiom,
! [Pid,Pid2] :
( host(Pid) != host(Pid2)
=> Pid != Pid2 ),
file('SWV011+0.ax',axiom_33) ).
fof(axiom_34,axiom,
~ setIn(nil,alive),
file('SWV011+0.ax',axiom_34) ).
fof(axiom_35,axiom,
! [X,Q] : head(cons(X,Q)) = X,
file('SWV011+0.ax',axiom_35) ).
fof(axiom_36,axiom,
! [X,Q] : tail(cons(X,Q)) = Q,
file('SWV011+0.ax',axiom_36) ).
fof(axiom_37,axiom,
! [Y,Q] : last(snoc(Q,Y)) = Y,
file('SWV011+0.ax',axiom_37) ).
fof(axiom_38,axiom,
! [Y,Q] : init(snoc(Q,Y)) = Q,
file('SWV011+0.ax',axiom_38) ).
fof(axiom_39,axiom,
! [Q] :
( Q = cons(head(Q),tail(Q))
| Q = q_nil ),
file('SWV011+0.ax',axiom_39) ).
fof(axiom_40,axiom,
! [Q] :
( Q = snoc(init(Q),last(Q))
| Q = q_nil ),
file('SWV011+0.ax',axiom_40) ).
fof(axiom_41,axiom,
! [X,Q] : q_nil != cons(X,Q),
file('SWV011+0.ax',axiom_41) ).
fof(axiom_42,axiom,
! [Y,Q] : q_nil != snoc(Q,Y),
file('SWV011+0.ax',axiom_42) ).
fof(axiom_43,axiom,
! [X] : cons(X,q_nil) = snoc(q_nil,X),
file('SWV011+0.ax',axiom_43) ).
fof(axiom_44,axiom,
! [X,Y,Q] : snoc(cons(X,Q),Y) = cons(X,snoc(Q,Y)),
file('SWV011+0.ax',axiom_44) ).
fof(axiom_45,axiom,
! [X] : ~ elem(X,q_nil),
file('SWV011+0.ax',axiom_45) ).
fof(axiom_46,axiom,
! [X,Y,Q] :
( elem(X,cons(Y,Q))
<=> ( elem(X,Q)
| X = Y ) ),
file('SWV011+0.ax',axiom_46) ).
fof(axiom_47,axiom,
! [X,Y,Q] :
( elem(X,snoc(Q,Y))
<=> ( elem(X,Q)
| X = Y ) ),
file('SWV011+0.ax',axiom_47) ).
fof(axiom_48,axiom,
! [X] :
( pidElem(X)
<=> ? [Y] :
( X = m_Down(Y)
| X = m_Halt(Y) ) ),
file('SWV011+0.ax',axiom_48) ).
fof(axiom_49,axiom,
! [X] : pidMsg(m_Halt(X)) = X,
file('SWV011+0.ax',axiom_49) ).
fof(axiom_50,axiom,
! [X] : pidMsg(m_Down(X)) = X,
file('SWV011+0.ax',axiom_50) ).
fof(axiom_51,axiom,
ordered(q_nil),
file('SWV011+0.ax',axiom_51) ).
fof(axiom_52,axiom,
! [X] :
( ordered(snoc(q_nil,X))
& ordered(cons(X,q_nil)) ),
file('SWV011+0.ax',axiom_52) ).
fof(axiom_53,axiom,
! [X,Q] :
( ordered(cons(X,Q))
<=> ( ! [Y] :
( ( host(pidMsg(Y)) = host(pidMsg(X))
& pidElem(Y)
& pidElem(X)
& elem(Y,Q) )
=> leq(pidMsg(X),pidMsg(Y)) )
& ordered(Q) ) ),
file('SWV011+0.ax',axiom_53) ).
fof(axiom_54,axiom,
! [X,Q] :
( ordered(snoc(Q,X))
<=> ( ! [Y] :
( ( host(pidMsg(Y)) = host(pidMsg(X))
& pidElem(Y)
& pidElem(X)
& elem(Y,Q) )
=> leq(pidMsg(Y),pidMsg(X)) )
& ordered(Q) ) ),
file('SWV011+0.ax',axiom_54) ).
fof(axiom_55,axiom,
! [Q,X,Y] :
( ordered(Q)
=> ordered(snoc(Q,m_Ack(X,Y))) ),
file('SWV011+0.ax',axiom_55) ).
fof(axiom_56,axiom,
! [Q,X] :
( ordered(Q)
=> ordered(snoc(Q,m_Ldr(X))) ),
file('SWV011+0.ax',axiom_56) ).
fof(axiom_57,axiom,
! [Q,X,Y] :
( ( elem(m_Down(Y),Q)
& host(X) = host(Y)
& ordered(cons(m_Halt(X),Q)) )
=> leq(X,Y) ),
file('SWV011+0.ax',axiom_57) ).
fof(axiom_58,axiom,
! [X] : ~ leq(s(X),X),
file('SWV011+0.ax',axiom_58) ).
fof(axiom_59,axiom,
! [X] : leq(X,X),
file('SWV011+0.ax',axiom_59) ).
fof(axiom_60,axiom,
! [X,Y] :
( leq(Y,X)
| leq(X,Y) ),
file('SWV011+0.ax',axiom_60) ).
fof(axiom_61,axiom,
! [X,Y] :
( ( leq(Y,X)
& leq(X,Y) )
<=> X = Y ),
file('SWV011+0.ax',axiom_61) ).
fof(axiom_62,axiom,
! [X,Y,Z] :
( ( leq(Y,Z)
& leq(X,Y) )
=> leq(X,Z) ),
file('SWV011+0.ax',axiom_62) ).
fof(axiom_63,axiom,
! [X,Y] :
( leq(X,Y)
<=> leq(s(X),s(Y)) ),
file('SWV011+0.ax',axiom_63) ).
fof(axiom_64,axiom,
! [X,Y] :
( leq(X,s(Y))
<=> ( leq(X,Y)
| X = s(Y) ) ),
file('SWV011+0.ax',axiom_64) ).
fof(axiom_65,axiom,
! [X] : ~ setIn(X,setEmpty),
file('SWV011+0.ax',axiom_65) ).
fof(conj,conjecture,
! [V,W,X,Y] :
( ( queue(host(X)) = cons(m_Ack(W,Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid20) = s(index(pendack,host(Pid0)))
& host(Pid30) = index(pendack,host(Pid0))
& index(status,host(Pid0)) = elec_2
& leq(nbr_proc,s(index(pendack,host(Pid0))))
& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& host(Pid0) = host(Pid30)
& host(Pid0) = nbr_proc
& elem(m_Down(Pid20),queue(host(Pid0)))
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( elem(m_Down(Pid30),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& elem(m_Halt(Pid0),queue(host(Pid20)))
& setIn(Pid0,alive)
& ~ leq(index(pendack,host(Pid0)),host(Z)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& host(Pid0) = host(Pid20)
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z] :
( ( setIn(Z,alive)
& ( index(status,host(Z)) = elec_2
| index(status,host(Z)) = elec_1 ) )
=> index(elid,host(Z)) = Z )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& setIn(Pid0,alive) )
=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
& ! [Z,Pid0] :
( ( elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> leq(host(Z),index(pendack,host(Pid0))) )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( elem(m_Ack(Pid0,Z),queue(host(Pid20)))
=> ~ leq(host(Z),host(Pid0)) )
& ! [Z,Pid0] :
( elem(m_Halt(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) )
& ! [Z,Pid0] :
( elem(m_Down(Pid0),queue(host(Z)))
=> host(Pid0) != host(Z) )
& ! [Z,Pid0] :
( elem(m_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( ( host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2
& index(elid,host(X)) = W )
=> ( leq(nbr_proc,index(pendack,host(X)))
=> ! [Z] :
( ( host(Z) = host(Y)
| setIn(host(Z),index(acks,host(X))) )
=> ! [V0] :
( host(X) != host(V0)
=> ! [W0,X0,Y0] :
( host(Z) = host(Y0)
=> ( host(X) != host(Y0)
=> ( ( host(X0) = s(index(pendack,host(Y0)))
& host(W0) = index(pendack,host(Y0))
& index(status,host(Y0)) = elec_2
& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
& leq(nbr_proc,s(index(pendack,host(Y0))))
& setIn(Y0,alive) )
=> ~ ( index(status,host(V0)) = norm
& index(ldr,host(V0)) = host(V0)
& setIn(V0,alive) ) ) ) ) ) ) ) ) ) ),
file('theBenchmark.p',conj) ).
fof(f_1_1,plain,
! [Pid,Pid2] :
( ( setIn(Pid2,pids)
& setIn(Pid,pids) )
| ~ elem(m_Ack(Pid,Pid2),queue(host(Pid))) ),
inference(fof_nnf,[status(thm)],[axiom]) ).
fof(f_1_2,plain,
! [U_1,U_0] :
( ( setIn(U_0,pids)
& setIn(U_1,pids) )
| ~ elem(m_Ack(U_1,U_0),queue(host(U_1))) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
( setIn(U_1,pids)
| ~ elem(m_Ack(U_1,U_0),queue(host(U_1))) ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_4,plain,
( setIn(U_0,pids)
| ~ elem(m_Ack(U_1,U_0),queue(host(U_1))) ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [P,Q] :
( host(P) != host(Q)
| s(host(P)) != host(Q) ),
inference(fof_nnf,[status(thm)],[axiom_01]) ).
fof(f_2_2,plain,
! [U_3,U_2] :
( host(U_3) != host(U_2)
| s(host(U_3)) != host(U_2) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
( host(U_3) != host(U_2)
| s(host(U_3)) != host(U_2) ),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [P] : leq(s(zero),host(P)),
inference(fof_nnf,[status(thm)],[axiom_02]) ).
fof(f_3_2,plain,
! [U_4] : leq(s(zero),host(U_4)),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
leq(s(zero),host(U_4)),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
leq(s(zero),nbr_proc),
inference(fof_nnf,[status(thm)],[axiom_03]) ).
cnf(f_4_2,plain,
leq(s(zero),nbr_proc),
inference(clausify,[status(thm)],[f_4_1]) ).
fof(f_5_1,plain,
! [P] : leq(host(P),nbr_proc),
inference(fof_nnf,[status(thm)],[axiom_04]) ).
fof(f_5_2,plain,
! [U_5] : leq(host(U_5),nbr_proc),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
leq(host(U_5),nbr_proc),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
elec_1 != elec_2,
inference(fof_nnf,[status(thm)],[axiom_05]) ).
cnf(f_6_2,plain,
elec_1 != elec_2,
inference(clausify,[status(thm)],[f_6_1]) ).
fof(f_7_1,plain,
elec_1 != wait,
inference(fof_nnf,[status(thm)],[axiom_06]) ).
cnf(f_7_2,plain,
elec_1 != wait,
inference(clausify,[status(thm)],[f_7_1]) ).
fof(f_8_1,plain,
elec_1 != norm,
inference(fof_nnf,[status(thm)],[axiom_07]) ).
cnf(f_8_2,plain,
elec_1 != norm,
inference(clausify,[status(thm)],[f_8_1]) ).
fof(f_9_1,plain,
elec_2 != wait,
inference(fof_nnf,[status(thm)],[axiom_08]) ).
cnf(f_9_2,plain,
elec_2 != wait,
inference(clausify,[status(thm)],[f_9_1]) ).
fof(f_10_1,plain,
elec_2 != norm,
inference(fof_nnf,[status(thm)],[axiom_09]) ).
cnf(f_10_2,plain,
elec_2 != norm,
inference(clausify,[status(thm)],[f_10_1]) ).
fof(f_11_1,plain,
norm != wait,
inference(fof_nnf,[status(thm)],[axiom_10]) ).
cnf(f_11_2,plain,
norm != wait,
inference(clausify,[status(thm)],[f_11_1]) ).
fof(f_12_1,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z),
inference(fof_nnf,[status(thm)],[axiom_11]) ).
fof(f_12_2,plain,
! [U_8,U_7,U_6] : m_Ack(U_8,U_7) != m_Halt(U_6),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
m_Ack(U_8,U_7) != m_Halt(U_6),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z),
inference(fof_nnf,[status(thm)],[axiom_12]) ).
fof(f_13_2,plain,
! [U_11,U_10,U_9] : m_Ack(U_11,U_10) != m_Down(U_9),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
m_Ack(U_11,U_10) != m_Down(U_9),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_NotNorm(Z),
inference(fof_nnf,[status(thm)],[axiom_13]) ).
fof(f_14_2,plain,
! [U_14,U_13,U_12] : m_Ack(U_14,U_13) != m_NotNorm(U_12),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
m_Ack(U_14,U_13) != m_NotNorm(U_12),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z),
inference(fof_nnf,[status(thm)],[axiom_14]) ).
fof(f_15_2,plain,
! [U_17,U_16,U_15] : m_Ack(U_17,U_16) != m_Ldr(U_15),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
m_Ack(U_17,U_16) != m_Ldr(U_15),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z),
inference(fof_nnf,[status(thm)],[axiom_15]) ).
fof(f_16_2,plain,
! [U_20,U_19,U_18] : m_Ack(U_20,U_19) != m_NormQ(U_18),
inference(variable_rename,[status(thm)],[f_16_1]) ).
cnf(f_16_3,plain,
m_Ack(U_20,U_19) != m_NormQ(U_18),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
! [X,Y] : m_NotNorm(X) != m_Halt(Y),
inference(fof_nnf,[status(thm)],[axiom_16]) ).
fof(f_17_2,plain,
! [U_22,U_21] : m_NotNorm(U_22) != m_Halt(U_21),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
m_NotNorm(U_22) != m_Halt(U_21),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [X,Y] : m_Down(X) != m_Halt(Y),
inference(fof_nnf,[status(thm)],[axiom_17]) ).
fof(f_18_2,plain,
! [U_24,U_23] : m_Down(U_24) != m_Halt(U_23),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
m_Down(U_24) != m_Halt(U_23),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [X,Y] : m_Down(X) != m_Ldr(Y),
inference(fof_nnf,[status(thm)],[axiom_18]) ).
fof(f_19_2,plain,
! [U_26,U_25] : m_Down(U_26) != m_Ldr(U_25),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
m_Down(U_26) != m_Ldr(U_25),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [X,Y] : m_Down(X) != m_NotNorm(Y),
inference(fof_nnf,[status(thm)],[axiom_19]) ).
fof(f_20_2,plain,
! [U_28,U_27] : m_Down(U_28) != m_NotNorm(U_27),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
m_Down(U_28) != m_NotNorm(U_27),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [X,Y] : m_Down(X) != m_NormQ(Y),
inference(fof_nnf,[status(thm)],[axiom_20]) ).
fof(f_21_2,plain,
! [U_30,U_29] : m_Down(U_30) != m_NormQ(U_29),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
m_Down(U_30) != m_NormQ(U_29),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [X,Y] : m_NormQ(X) != m_Halt(Y),
inference(fof_nnf,[status(thm)],[axiom_21]) ).
fof(f_22_2,plain,
! [U_32,U_31] : m_NormQ(U_32) != m_Halt(U_31),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
m_NormQ(U_32) != m_Halt(U_31),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [X,Y] : m_Ldr(X) != m_Halt(Y),
inference(fof_nnf,[status(thm)],[axiom_22]) ).
fof(f_23_2,plain,
! [U_34,U_33] : m_Ldr(U_34) != m_Halt(U_33),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
m_Ldr(U_34) != m_Halt(U_33),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
! [X,Y] : m_Ldr(X) != m_NormQ(Y),
inference(fof_nnf,[status(thm)],[axiom_23]) ).
fof(f_24_2,plain,
! [U_36,U_35] : m_Ldr(U_36) != m_NormQ(U_35),
inference(variable_rename,[status(thm)],[f_24_1]) ).
cnf(f_24_3,plain,
m_Ldr(U_36) != m_NormQ(U_35),
inference(clausify,[status(thm)],[f_24_2]) ).
fof(f_25_1,plain,
! [X,Y] : m_Ldr(X) != m_NotNorm(Y),
inference(fof_nnf,[status(thm)],[axiom_24]) ).
fof(f_25_2,plain,
! [U_38,U_37] : m_Ldr(U_38) != m_NotNorm(U_37),
inference(variable_rename,[status(thm)],[f_25_1]) ).
cnf(f_25_3,plain,
m_Ldr(U_38) != m_NotNorm(U_37),
inference(clausify,[status(thm)],[f_25_2]) ).
fof(f_26_1,plain,
! [X,Y] : m_NormQ(X) != m_NotNorm(Y),
inference(fof_nnf,[status(thm)],[axiom_25]) ).
fof(f_26_2,plain,
! [U_40,U_39] : m_NormQ(U_40) != m_NotNorm(U_39),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
m_NormQ(U_40) != m_NotNorm(U_39),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,plain,
! [X,Y] :
( ( X != Y
| m_Halt(X) = m_Halt(Y) )
& ( m_Halt(X) != m_Halt(Y)
| X = Y ) ),
inference(fof_nnf,[status(thm)],[axiom_26]) ).
fof(f_27_2,plain,
! [U_42,U_41] :
( ( U_42 != U_41
| m_Halt(U_42) = m_Halt(U_41) )
& ( m_Halt(U_42) != m_Halt(U_41)
| U_42 = U_41 ) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( ! [U_46,U_44] :
( U_46 != U_44
| m_Halt(U_46) = m_Halt(U_44) )
& ! [U_45,U_43] :
( m_Halt(U_45) != m_Halt(U_43)
| U_45 = U_43 ) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
cnf(f_27_4,plain,
( m_Halt(U_45) != m_Halt(U_43)
| U_45 = U_43 ),
inference(clausify,[status(thm)],[f_27_3]) ).
cnf(f_27_5,plain,
( U_46 != U_44
| m_Halt(U_46) = m_Halt(U_44) ),
inference(clausify,[status(thm)],[f_27_3]) ).
fof(f_28_1,plain,
! [X,Y] :
( ( X != Y
| m_NormQ(X) = m_NormQ(Y) )
& ( m_NormQ(X) != m_NormQ(Y)
| X = Y ) ),
inference(fof_nnf,[status(thm)],[axiom_27]) ).
fof(f_28_2,plain,
! [U_48,U_47] :
( ( U_48 != U_47
| m_NormQ(U_48) = m_NormQ(U_47) )
& ( m_NormQ(U_48) != m_NormQ(U_47)
| U_48 = U_47 ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_52,U_50] :
( U_52 != U_50
| m_NormQ(U_52) = m_NormQ(U_50) )
& ! [U_51,U_49] :
( m_NormQ(U_51) != m_NormQ(U_49)
| U_51 = U_49 ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
cnf(f_28_4,plain,
( m_NormQ(U_51) != m_NormQ(U_49)
| U_51 = U_49 ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_5,plain,
( U_52 != U_50
| m_NormQ(U_52) = m_NormQ(U_50) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X,Y] :
( ( X != Y
| m_NotNorm(X) = m_NotNorm(Y) )
& ( m_NotNorm(X) != m_NotNorm(Y)
| X = Y ) ),
inference(fof_nnf,[status(thm)],[axiom_28]) ).
fof(f_29_2,plain,
! [U_54,U_53] :
( ( U_54 != U_53
| m_NotNorm(U_54) = m_NotNorm(U_53) )
& ( m_NotNorm(U_54) != m_NotNorm(U_53)
| U_54 = U_53 ) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ! [U_58,U_56] :
( U_58 != U_56
| m_NotNorm(U_58) = m_NotNorm(U_56) )
& ! [U_57,U_55] :
( m_NotNorm(U_57) != m_NotNorm(U_55)
| U_57 = U_55 ) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
( m_NotNorm(U_57) != m_NotNorm(U_55)
| U_57 = U_55 ),
inference(clausify,[status(thm)],[f_29_3]) ).
cnf(f_29_5,plain,
( U_58 != U_56
| m_NotNorm(U_58) = m_NotNorm(U_56) ),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_30_1,plain,
! [X,Y] :
( ( X != Y
| m_Ldr(X) = m_Ldr(Y) )
& ( m_Ldr(X) != m_Ldr(Y)
| X = Y ) ),
inference(fof_nnf,[status(thm)],[axiom_29]) ).
fof(f_30_2,plain,
! [U_60,U_59] :
( ( U_60 != U_59
| m_Ldr(U_60) = m_Ldr(U_59) )
& ( m_Ldr(U_60) != m_Ldr(U_59)
| U_60 = U_59 ) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ! [U_64,U_62] :
( U_64 != U_62
| m_Ldr(U_64) = m_Ldr(U_62) )
& ! [U_63,U_61] :
( m_Ldr(U_63) != m_Ldr(U_61)
| U_63 = U_61 ) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
cnf(f_30_4,plain,
( m_Ldr(U_63) != m_Ldr(U_61)
| U_63 = U_61 ),
inference(clausify,[status(thm)],[f_30_3]) ).
cnf(f_30_5,plain,
( U_64 != U_62
| m_Ldr(U_64) = m_Ldr(U_62) ),
inference(clausify,[status(thm)],[f_30_3]) ).
fof(f_31_1,plain,
! [X,Y] :
( ( X != Y
| m_Down(X) = m_Down(Y) )
& ( m_Down(X) != m_Down(Y)
| X = Y ) ),
inference(fof_nnf,[status(thm)],[axiom_30]) ).
fof(f_31_2,plain,
! [U_66,U_65] :
( ( U_66 != U_65
| m_Down(U_66) = m_Down(U_65) )
& ( m_Down(U_66) != m_Down(U_65)
| U_66 = U_65 ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_70,U_68] :
( U_70 != U_68
| m_Down(U_70) = m_Down(U_68) )
& ! [U_69,U_67] :
( m_Down(U_69) != m_Down(U_67)
| U_69 = U_67 ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( m_Down(U_69) != m_Down(U_67)
| U_69 = U_67 ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_5,plain,
( U_70 != U_68
| m_Down(U_70) = m_Down(U_68) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [X1,X2,Y1,Y2] :
( m_Ack(X1,Y1) != m_Ack(X2,Y2)
| X1 = X2 ),
inference(fof_nnf,[status(thm)],[axiom_31]) ).
fof(f_32_2,plain,
! [U_74,U_73,U_72,U_71] :
( m_Ack(U_74,U_72) != m_Ack(U_73,U_71)
| U_74 = U_73 ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
! [U_74,U_73] :
( ! [U_72,U_71] : m_Ack(U_74,U_72) != m_Ack(U_73,U_71)
| U_74 = U_73 ),
inference(miniscope,[status(thm)],[f_32_2]) ).
cnf(f_32_4,plain,
( m_Ack(U_74,U_72) != m_Ack(U_73,U_71)
| U_74 = U_73 ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [X1,X2,Y1,Y2] :
( m_Ack(X1,Y1) != m_Ack(X2,Y2)
| Y1 = Y2 ),
inference(fof_nnf,[status(thm)],[axiom_32]) ).
fof(f_33_2,plain,
! [U_78,U_77,U_76,U_75] :
( m_Ack(U_78,U_76) != m_Ack(U_77,U_75)
| U_76 = U_75 ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
cnf(f_33_3,plain,
( m_Ack(U_78,U_76) != m_Ack(U_77,U_75)
| U_76 = U_75 ),
inference(clausify,[status(thm)],[f_33_2]) ).
fof(f_34_1,plain,
! [Pid,Pid2] :
( Pid != Pid2
| host(Pid) = host(Pid2) ),
inference(fof_nnf,[status(thm)],[axiom_33]) ).
fof(f_34_2,plain,
! [U_80,U_79] :
( U_80 != U_79
| host(U_80) = host(U_79) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
cnf(f_34_3,plain,
( U_80 != U_79
| host(U_80) = host(U_79) ),
inference(clausify,[status(thm)],[f_34_2]) ).
fof(f_35_1,plain,
~ setIn(nil,alive),
inference(fof_nnf,[status(thm)],[axiom_34]) ).
cnf(f_35_2,plain,
~ setIn(nil,alive),
inference(clausify,[status(thm)],[f_35_1]) ).
fof(f_36_1,plain,
! [X,Q] : head(cons(X,Q)) = X,
inference(fof_nnf,[status(thm)],[axiom_35]) ).
fof(f_36_2,plain,
! [U_82,U_81] : head(cons(U_82,U_81)) = U_82,
inference(variable_rename,[status(thm)],[f_36_1]) ).
cnf(f_36_3,plain,
head(cons(U_82,U_81)) = U_82,
inference(clausify,[status(thm)],[f_36_2]) ).
fof(f_37_1,plain,
! [X,Q] : tail(cons(X,Q)) = Q,
inference(fof_nnf,[status(thm)],[axiom_36]) ).
fof(f_37_2,plain,
! [U_84,U_83] : tail(cons(U_84,U_83)) = U_83,
inference(variable_rename,[status(thm)],[f_37_1]) ).
cnf(f_37_3,plain,
tail(cons(U_84,U_83)) = U_83,
inference(clausify,[status(thm)],[f_37_2]) ).
fof(f_38_1,plain,
! [Y,Q] : last(snoc(Q,Y)) = Y,
inference(fof_nnf,[status(thm)],[axiom_37]) ).
fof(f_38_2,plain,
! [U_86,U_85] : last(snoc(U_85,U_86)) = U_86,
inference(variable_rename,[status(thm)],[f_38_1]) ).
cnf(f_38_3,plain,
last(snoc(U_85,U_86)) = U_86,
inference(clausify,[status(thm)],[f_38_2]) ).
fof(f_39_1,plain,
! [Y,Q] : init(snoc(Q,Y)) = Q,
inference(fof_nnf,[status(thm)],[axiom_38]) ).
fof(f_39_2,plain,
! [U_88,U_87] : init(snoc(U_87,U_88)) = U_87,
inference(variable_rename,[status(thm)],[f_39_1]) ).
cnf(f_39_3,plain,
init(snoc(U_87,U_88)) = U_87,
inference(clausify,[status(thm)],[f_39_2]) ).
fof(f_40_1,plain,
! [Q] :
( Q = cons(head(Q),tail(Q))
| Q = q_nil ),
inference(fof_nnf,[status(thm)],[axiom_39]) ).
fof(f_40_2,plain,
! [U_89] :
( U_89 = cons(head(U_89),tail(U_89))
| U_89 = q_nil ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
cnf(f_40_3,plain,
( U_89 = cons(head(U_89),tail(U_89))
| U_89 = q_nil ),
inference(clausify,[status(thm)],[f_40_2]) ).
fof(f_41_1,plain,
! [Q] :
( Q = snoc(init(Q),last(Q))
| Q = q_nil ),
inference(fof_nnf,[status(thm)],[axiom_40]) ).
fof(f_41_2,plain,
! [U_90] :
( U_90 = snoc(init(U_90),last(U_90))
| U_90 = q_nil ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
cnf(f_41_3,plain,
( U_90 = snoc(init(U_90),last(U_90))
| U_90 = q_nil ),
inference(clausify,[status(thm)],[f_41_2]) ).
fof(f_42_1,plain,
! [X,Q] : q_nil != cons(X,Q),
inference(fof_nnf,[status(thm)],[axiom_41]) ).
fof(f_42_2,plain,
! [U_92,U_91] : q_nil != cons(U_92,U_91),
inference(variable_rename,[status(thm)],[f_42_1]) ).
cnf(f_42_3,plain,
q_nil != cons(U_92,U_91),
inference(clausify,[status(thm)],[f_42_2]) ).
fof(f_43_1,plain,
! [Y,Q] : q_nil != snoc(Q,Y),
inference(fof_nnf,[status(thm)],[axiom_42]) ).
fof(f_43_2,plain,
! [U_94,U_93] : q_nil != snoc(U_93,U_94),
inference(variable_rename,[status(thm)],[f_43_1]) ).
cnf(f_43_3,plain,
q_nil != snoc(U_93,U_94),
inference(clausify,[status(thm)],[f_43_2]) ).
fof(f_44_1,plain,
! [X] : cons(X,q_nil) = snoc(q_nil,X),
inference(fof_nnf,[status(thm)],[axiom_43]) ).
fof(f_44_2,plain,
! [U_95] : cons(U_95,q_nil) = snoc(q_nil,U_95),
inference(variable_rename,[status(thm)],[f_44_1]) ).
cnf(f_44_3,plain,
cons(U_95,q_nil) = snoc(q_nil,U_95),
inference(clausify,[status(thm)],[f_44_2]) ).
fof(f_45_1,plain,
! [X,Y,Q] : snoc(cons(X,Q),Y) = cons(X,snoc(Q,Y)),
inference(fof_nnf,[status(thm)],[axiom_44]) ).
fof(f_45_2,plain,
! [U_98,U_97,U_96] : snoc(cons(U_98,U_96),U_97) = cons(U_98,snoc(U_96,U_97)),
inference(variable_rename,[status(thm)],[f_45_1]) ).
cnf(f_45_3,plain,
snoc(cons(U_98,U_96),U_97) = cons(U_98,snoc(U_96,U_97)),
inference(clausify,[status(thm)],[f_45_2]) ).
fof(f_46_1,plain,
! [X] : ~ elem(X,q_nil),
inference(fof_nnf,[status(thm)],[axiom_45]) ).
fof(f_46_2,plain,
! [U_99] : ~ elem(U_99,q_nil),
inference(variable_rename,[status(thm)],[f_46_1]) ).
cnf(f_46_3,plain,
~ elem(U_99,q_nil),
inference(clausify,[status(thm)],[f_46_2]) ).
fof(f_47_1,plain,
! [X,Y,Q] :
( ( elem(X,cons(Y,Q))
| ( ~ elem(X,Q)
& X != Y ) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,cons(Y,Q)) ) ),
inference(fof_nnf,[status(thm)],[axiom_46]) ).
fof(f_47_2,plain,
! [U_102,U_101,U_100] :
( ( elem(U_102,cons(U_101,U_100))
| ( ~ elem(U_102,U_100)
& U_102 != U_101 ) )
& ( elem(U_102,U_100)
| U_102 = U_101
| ~ elem(U_102,cons(U_101,U_100)) ) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
( ! [U_108,U_106,U_104] :
( elem(U_108,cons(U_106,U_104))
| ( ~ elem(U_108,U_104)
& U_108 != U_106 ) )
& ! [U_107,U_105,U_103] :
( elem(U_107,U_103)
| U_107 = U_105
| ~ elem(U_107,cons(U_105,U_103)) ) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
cnf(f_47_4,plain,
( elem(U_107,U_103)
| U_107 = U_105
| ~ elem(U_107,cons(U_105,U_103)) ),
inference(clausify,[status(thm)],[f_47_3]) ).
cnf(f_47_5,plain,
( U_108 != U_106
| elem(U_108,cons(U_106,U_104)) ),
inference(clausify,[status(thm)],[f_47_3]) ).
cnf(f_47_6,plain,
( ~ elem(U_108,U_104)
| elem(U_108,cons(U_106,U_104)) ),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,plain,
! [X,Y,Q] :
( ( elem(X,snoc(Q,Y))
| ( ~ elem(X,Q)
& X != Y ) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,snoc(Q,Y)) ) ),
inference(fof_nnf,[status(thm)],[axiom_47]) ).
fof(f_48_2,plain,
! [U_111,U_110,U_109] :
( ( elem(U_111,snoc(U_109,U_110))
| ( ~ elem(U_111,U_109)
& U_111 != U_110 ) )
& ( elem(U_111,U_109)
| U_111 = U_110
| ~ elem(U_111,snoc(U_109,U_110)) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_117,U_115,U_113] :
( elem(U_117,snoc(U_113,U_115))
| ( ~ elem(U_117,U_113)
& U_117 != U_115 ) )
& ! [U_116,U_114,U_112] :
( elem(U_116,U_112)
| U_116 = U_114
| ~ elem(U_116,snoc(U_112,U_114)) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( elem(U_116,U_112)
| U_116 = U_114
| ~ elem(U_116,snoc(U_112,U_114)) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_5,plain,
( U_117 != U_115
| elem(U_117,snoc(U_113,U_115)) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_6,plain,
( ~ elem(U_117,U_113)
| elem(U_117,snoc(U_113,U_115)) ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
! [X] :
( ( pidElem(X)
| ! [Y] :
( X != m_Down(Y)
& X != m_Halt(Y) ) )
& ( ? [Y] :
( X = m_Down(Y)
| X = m_Halt(Y) )
| ~ pidElem(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_48]) ).
fof(f_49_2,plain,
! [U_120] :
( ( pidElem(U_120)
| ! [U_119] :
( U_120 != m_Down(U_119)
& U_120 != m_Halt(U_119) ) )
& ( ? [U_118] :
( U_120 = m_Down(U_118)
| U_120 = m_Halt(U_118) )
| ~ pidElem(U_120) ) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
( ! [U_126] :
( pidElem(U_126)
| ( ! [U_124] : U_126 != m_Down(U_124)
& ! [U_123] : U_126 != m_Halt(U_123) ) )
& ! [U_125] :
( ? [U_122] : U_125 = m_Down(U_122)
| ? [U_121] : U_125 = m_Halt(U_121)
| ~ pidElem(U_125) ) ),
inference(miniscope,[status(thm)],[f_49_2]) ).
fof(f_49_4,plain,
( ! [U_126] :
( pidElem(U_126)
| ( ! [U_124] : U_126 != m_Down(U_124)
& ! [U_123] : U_126 != m_Halt(U_123) ) )
& ! [U_125] :
( ? [U_122] : U_125 = m_Down(U_122)
| U_125 = m_Halt(sK1(U_125))
| ~ pidElem(U_125) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_121,sK1(U_125))],[f_49_3]) ).
fof(f_49_5,plain,
( ! [U_126] :
( pidElem(U_126)
| ( ! [U_124] : U_126 != m_Down(U_124)
& ! [U_123] : U_126 != m_Halt(U_123) ) )
& ! [U_125] :
( U_125 = m_Down(sK2(U_125))
| U_125 = m_Halt(sK1(U_125))
| ~ pidElem(U_125) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_122,sK2(U_125))],[f_49_4]) ).
cnf(f_49_6,plain,
( U_125 = m_Down(sK2(U_125))
| U_125 = m_Halt(sK1(U_125))
| ~ pidElem(U_125) ),
inference(clausify,[status(thm)],[f_49_5]) ).
cnf(f_49_7,plain,
( U_126 != m_Halt(U_123)
| pidElem(U_126) ),
inference(clausify,[status(thm)],[f_49_5]) ).
cnf(f_49_8,plain,
( U_126 != m_Down(U_124)
| pidElem(U_126) ),
inference(clausify,[status(thm)],[f_49_5]) ).
fof(f_50_1,plain,
! [X] : pidMsg(m_Halt(X)) = X,
inference(fof_nnf,[status(thm)],[axiom_49]) ).
fof(f_50_2,plain,
! [U_127] : pidMsg(m_Halt(U_127)) = U_127,
inference(variable_rename,[status(thm)],[f_50_1]) ).
cnf(f_50_3,plain,
pidMsg(m_Halt(U_127)) = U_127,
inference(clausify,[status(thm)],[f_50_2]) ).
fof(f_51_1,plain,
! [X] : pidMsg(m_Down(X)) = X,
inference(fof_nnf,[status(thm)],[axiom_50]) ).
fof(f_51_2,plain,
! [U_128] : pidMsg(m_Down(U_128)) = U_128,
inference(variable_rename,[status(thm)],[f_51_1]) ).
cnf(f_51_3,plain,
pidMsg(m_Down(U_128)) = U_128,
inference(clausify,[status(thm)],[f_51_2]) ).
fof(f_52_1,plain,
ordered(q_nil),
inference(fof_nnf,[status(thm)],[axiom_51]) ).
cnf(f_52_2,plain,
ordered(q_nil),
inference(clausify,[status(thm)],[f_52_1]) ).
fof(f_53_1,plain,
! [X] :
( ordered(snoc(q_nil,X))
& ordered(cons(X,q_nil)) ),
inference(fof_nnf,[status(thm)],[axiom_52]) ).
fof(f_53_2,plain,
! [U_129] :
( ordered(snoc(q_nil,U_129))
& ordered(cons(U_129,q_nil)) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
( ! [U_131] : ordered(snoc(q_nil,U_131))
& ! [U_130] : ordered(cons(U_130,q_nil)) ),
inference(miniscope,[status(thm)],[f_53_2]) ).
cnf(f_53_4,plain,
ordered(cons(U_130,q_nil)),
inference(clausify,[status(thm)],[f_53_3]) ).
cnf(f_53_5,plain,
ordered(snoc(q_nil,U_131)),
inference(clausify,[status(thm)],[f_53_3]) ).
fof(f_54_1,plain,
! [X,Q] :
( ( ordered(cons(X,Q))
| ? [Y] :
( ~ leq(pidMsg(X),pidMsg(Y))
& host(pidMsg(Y)) = host(pidMsg(X))
& pidElem(Y)
& pidElem(X)
& elem(Y,Q) )
| ~ ordered(Q) )
& ( ( ! [Y] :
( leq(pidMsg(X),pidMsg(Y))
| host(pidMsg(Y)) != host(pidMsg(X))
| ~ pidElem(Y)
| ~ pidElem(X)
| ~ elem(Y,Q) )
& ordered(Q) )
| ~ ordered(cons(X,Q)) ) ),
inference(fof_nnf,[status(thm)],[axiom_53]) ).
fof(f_54_2,plain,
! [U_135,U_134] :
( ( ordered(cons(U_135,U_134))
| ? [U_133] :
( ~ leq(pidMsg(U_135),pidMsg(U_133))
& host(pidMsg(U_133)) = host(pidMsg(U_135))
& pidElem(U_133)
& pidElem(U_135)
& elem(U_133,U_134) )
| ~ ordered(U_134) )
& ( ( ! [U_132] :
( leq(pidMsg(U_135),pidMsg(U_132))
| host(pidMsg(U_132)) != host(pidMsg(U_135))
| ~ pidElem(U_132)
| ~ pidElem(U_135)
| ~ elem(U_132,U_134) )
& ordered(U_134) )
| ~ ordered(cons(U_135,U_134)) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_139,U_137] :
( ordered(cons(U_139,U_137))
| ? [U_133] :
( ~ leq(pidMsg(U_139),pidMsg(U_133))
& host(pidMsg(U_133)) = host(pidMsg(U_139))
& pidElem(U_133)
& pidElem(U_139)
& elem(U_133,U_137) )
| ~ ordered(U_137) )
& ! [U_138,U_136] :
( ( ! [U_132] :
( leq(pidMsg(U_138),pidMsg(U_132))
| host(pidMsg(U_132)) != host(pidMsg(U_138))
| ~ pidElem(U_132)
| ~ pidElem(U_138)
| ~ elem(U_132,U_136) )
& ordered(U_136) )
| ~ ordered(cons(U_138,U_136)) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
fof(f_54_4,plain,
( ! [U_139,U_137] :
( ordered(cons(U_139,U_137))
| ( ~ leq(pidMsg(U_139),pidMsg(sK3(U_139,U_137)))
& host(pidMsg(sK3(U_139,U_137))) = host(pidMsg(U_139))
& pidElem(sK3(U_139,U_137))
& pidElem(U_139)
& elem(sK3(U_139,U_137),U_137) )
| ~ ordered(U_137) )
& ! [U_138,U_136] :
( ( ! [U_132] :
( leq(pidMsg(U_138),pidMsg(U_132))
| host(pidMsg(U_132)) != host(pidMsg(U_138))
| ~ pidElem(U_132)
| ~ pidElem(U_138)
| ~ elem(U_132,U_136) )
& ordered(U_136) )
| ~ ordered(cons(U_138,U_136)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_133,sK3(U_139,U_137))],[f_54_3]) ).
cnf(f_54_5,plain,
( ordered(U_136)
| ~ ordered(cons(U_138,U_136)) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_6,plain,
( leq(pidMsg(U_138),pidMsg(U_132))
| host(pidMsg(U_132)) != host(pidMsg(U_138))
| ~ pidElem(U_132)
| ~ pidElem(U_138)
| ~ elem(U_132,U_136)
| ~ ordered(cons(U_138,U_136)) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_7,plain,
( elem(sK3(U_139,U_137),U_137)
| ~ ordered(U_137)
| ordered(cons(U_139,U_137)) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_8,plain,
( pidElem(U_139)
| ~ ordered(U_137)
| ordered(cons(U_139,U_137)) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_9,plain,
( pidElem(sK3(U_139,U_137))
| ~ ordered(U_137)
| ordered(cons(U_139,U_137)) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_10,plain,
( host(pidMsg(sK3(U_139,U_137))) = host(pidMsg(U_139))
| ~ ordered(U_137)
| ordered(cons(U_139,U_137)) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_11,plain,
( ~ leq(pidMsg(U_139),pidMsg(sK3(U_139,U_137)))
| ~ ordered(U_137)
| ordered(cons(U_139,U_137)) ),
inference(clausify,[status(thm)],[f_54_4]) ).
fof(f_55_1,plain,
! [X,Q] :
( ( ordered(snoc(Q,X))
| ? [Y] :
( ~ leq(pidMsg(Y),pidMsg(X))
& host(pidMsg(Y)) = host(pidMsg(X))
& pidElem(Y)
& pidElem(X)
& elem(Y,Q) )
| ~ ordered(Q) )
& ( ( ! [Y] :
( leq(pidMsg(Y),pidMsg(X))
| host(pidMsg(Y)) != host(pidMsg(X))
| ~ pidElem(Y)
| ~ pidElem(X)
| ~ elem(Y,Q) )
& ordered(Q) )
| ~ ordered(snoc(Q,X)) ) ),
inference(fof_nnf,[status(thm)],[axiom_54]) ).
fof(f_55_2,plain,
! [U_143,U_142] :
( ( ordered(snoc(U_142,U_143))
| ? [U_141] :
( ~ leq(pidMsg(U_141),pidMsg(U_143))
& host(pidMsg(U_141)) = host(pidMsg(U_143))
& pidElem(U_141)
& pidElem(U_143)
& elem(U_141,U_142) )
| ~ ordered(U_142) )
& ( ( ! [U_140] :
( leq(pidMsg(U_140),pidMsg(U_143))
| host(pidMsg(U_140)) != host(pidMsg(U_143))
| ~ pidElem(U_140)
| ~ pidElem(U_143)
| ~ elem(U_140,U_142) )
& ordered(U_142) )
| ~ ordered(snoc(U_142,U_143)) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_147,U_145] :
( ordered(snoc(U_145,U_147))
| ? [U_141] :
( ~ leq(pidMsg(U_141),pidMsg(U_147))
& host(pidMsg(U_141)) = host(pidMsg(U_147))
& pidElem(U_141)
& pidElem(U_147)
& elem(U_141,U_145) )
| ~ ordered(U_145) )
& ! [U_146,U_144] :
( ( ! [U_140] :
( leq(pidMsg(U_140),pidMsg(U_146))
| host(pidMsg(U_140)) != host(pidMsg(U_146))
| ~ pidElem(U_140)
| ~ pidElem(U_146)
| ~ elem(U_140,U_144) )
& ordered(U_144) )
| ~ ordered(snoc(U_144,U_146)) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
fof(f_55_4,plain,
( ! [U_147,U_145] :
( ordered(snoc(U_145,U_147))
| ( ~ leq(pidMsg(sK4(U_147,U_145)),pidMsg(U_147))
& host(pidMsg(sK4(U_147,U_145))) = host(pidMsg(U_147))
& pidElem(sK4(U_147,U_145))
& pidElem(U_147)
& elem(sK4(U_147,U_145),U_145) )
| ~ ordered(U_145) )
& ! [U_146,U_144] :
( ( ! [U_140] :
( leq(pidMsg(U_140),pidMsg(U_146))
| host(pidMsg(U_140)) != host(pidMsg(U_146))
| ~ pidElem(U_140)
| ~ pidElem(U_146)
| ~ elem(U_140,U_144) )
& ordered(U_144) )
| ~ ordered(snoc(U_144,U_146)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_141,sK4(U_147,U_145))],[f_55_3]) ).
cnf(f_55_5,plain,
( ordered(U_144)
| ~ ordered(snoc(U_144,U_146)) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_6,plain,
( leq(pidMsg(U_140),pidMsg(U_146))
| host(pidMsg(U_140)) != host(pidMsg(U_146))
| ~ pidElem(U_140)
| ~ pidElem(U_146)
| ~ elem(U_140,U_144)
| ~ ordered(snoc(U_144,U_146)) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_7,plain,
( elem(sK4(U_147,U_145),U_145)
| ~ ordered(U_145)
| ordered(snoc(U_145,U_147)) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_8,plain,
( pidElem(U_147)
| ~ ordered(U_145)
| ordered(snoc(U_145,U_147)) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_9,plain,
( pidElem(sK4(U_147,U_145))
| ~ ordered(U_145)
| ordered(snoc(U_145,U_147)) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_10,plain,
( host(pidMsg(sK4(U_147,U_145))) = host(pidMsg(U_147))
| ~ ordered(U_145)
| ordered(snoc(U_145,U_147)) ),
inference(clausify,[status(thm)],[f_55_4]) ).
cnf(f_55_11,plain,
( ~ leq(pidMsg(sK4(U_147,U_145)),pidMsg(U_147))
| ~ ordered(U_145)
| ordered(snoc(U_145,U_147)) ),
inference(clausify,[status(thm)],[f_55_4]) ).
fof(f_56_1,plain,
! [Q,X,Y] :
( ordered(snoc(Q,m_Ack(X,Y)))
| ~ ordered(Q) ),
inference(fof_nnf,[status(thm)],[axiom_55]) ).
fof(f_56_2,plain,
! [U_150,U_149,U_148] :
( ordered(snoc(U_150,m_Ack(U_149,U_148)))
| ~ ordered(U_150) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
! [U_150] :
( ! [U_149,U_148] : ordered(snoc(U_150,m_Ack(U_149,U_148)))
| ~ ordered(U_150) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
cnf(f_56_4,plain,
( ordered(snoc(U_150,m_Ack(U_149,U_148)))
| ~ ordered(U_150) ),
inference(clausify,[status(thm)],[f_56_3]) ).
fof(f_57_1,plain,
! [Q,X] :
( ordered(snoc(Q,m_Ldr(X)))
| ~ ordered(Q) ),
inference(fof_nnf,[status(thm)],[axiom_56]) ).
fof(f_57_2,plain,
! [U_152,U_151] :
( ordered(snoc(U_152,m_Ldr(U_151)))
| ~ ordered(U_152) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
! [U_152] :
( ! [U_151] : ordered(snoc(U_152,m_Ldr(U_151)))
| ~ ordered(U_152) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( ordered(snoc(U_152,m_Ldr(U_151)))
| ~ ordered(U_152) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [Q,X,Y] :
( leq(X,Y)
| ~ elem(m_Down(Y),Q)
| host(X) != host(Y)
| ~ ordered(cons(m_Halt(X),Q)) ),
inference(fof_nnf,[status(thm)],[axiom_57]) ).
fof(f_58_2,plain,
! [U_155,U_154,U_153] :
( leq(U_154,U_153)
| ~ elem(m_Down(U_153),U_155)
| host(U_154) != host(U_153)
| ~ ordered(cons(m_Halt(U_154),U_155)) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
cnf(f_58_3,plain,
( leq(U_154,U_153)
| ~ elem(m_Down(U_153),U_155)
| host(U_154) != host(U_153)
| ~ ordered(cons(m_Halt(U_154),U_155)) ),
inference(clausify,[status(thm)],[f_58_2]) ).
fof(f_59_1,plain,
! [X] : ~ leq(s(X),X),
inference(fof_nnf,[status(thm)],[axiom_58]) ).
fof(f_59_2,plain,
! [U_156] : ~ leq(s(U_156),U_156),
inference(variable_rename,[status(thm)],[f_59_1]) ).
cnf(f_59_3,plain,
~ leq(s(U_156),U_156),
inference(clausify,[status(thm)],[f_59_2]) ).
fof(f_60_1,plain,
! [X] : leq(X,X),
inference(fof_nnf,[status(thm)],[axiom_59]) ).
fof(f_60_2,plain,
! [U_157] : leq(U_157,U_157),
inference(variable_rename,[status(thm)],[f_60_1]) ).
cnf(f_60_3,plain,
leq(U_157,U_157),
inference(clausify,[status(thm)],[f_60_2]) ).
fof(f_61_1,plain,
! [X,Y] :
( leq(Y,X)
| leq(X,Y) ),
inference(fof_nnf,[status(thm)],[axiom_60]) ).
fof(f_61_2,plain,
! [U_159,U_158] :
( leq(U_158,U_159)
| leq(U_159,U_158) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
cnf(f_61_3,plain,
( leq(U_158,U_159)
| leq(U_159,U_158) ),
inference(clausify,[status(thm)],[f_61_2]) ).
fof(f_62_1,plain,
! [X,Y] :
( ( ( leq(Y,X)
& leq(X,Y) )
| X != Y )
& ( X = Y
| ~ leq(Y,X)
| ~ leq(X,Y) ) ),
inference(fof_nnf,[status(thm)],[axiom_61]) ).
fof(f_62_2,plain,
! [U_161,U_160] :
( ( ( leq(U_160,U_161)
& leq(U_161,U_160) )
| U_161 != U_160 )
& ( U_161 = U_160
| ~ leq(U_160,U_161)
| ~ leq(U_161,U_160) ) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
fof(f_62_3,plain,
( ! [U_165,U_163] :
( ( leq(U_163,U_165)
& leq(U_165,U_163) )
| U_165 != U_163 )
& ! [U_164,U_162] :
( U_164 = U_162
| ~ leq(U_162,U_164)
| ~ leq(U_164,U_162) ) ),
inference(miniscope,[status(thm)],[f_62_2]) ).
cnf(f_62_4,plain,
( U_164 = U_162
| ~ leq(U_162,U_164)
| ~ leq(U_164,U_162) ),
inference(clausify,[status(thm)],[f_62_3]) ).
cnf(f_62_5,plain,
( leq(U_165,U_163)
| U_165 != U_163 ),
inference(clausify,[status(thm)],[f_62_3]) ).
cnf(f_62_6,plain,
( leq(U_163,U_165)
| U_165 != U_163 ),
inference(clausify,[status(thm)],[f_62_3]) ).
fof(f_63_1,plain,
! [X,Y,Z] :
( leq(X,Z)
| ~ leq(Y,Z)
| ~ leq(X,Y) ),
inference(fof_nnf,[status(thm)],[axiom_62]) ).
fof(f_63_2,plain,
! [U_168,U_167,U_166] :
( leq(U_168,U_166)
| ~ leq(U_167,U_166)
| ~ leq(U_168,U_167) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
cnf(f_63_3,plain,
( leq(U_168,U_166)
| ~ leq(U_167,U_166)
| ~ leq(U_168,U_167) ),
inference(clausify,[status(thm)],[f_63_2]) ).
fof(f_64_1,plain,
! [X,Y] :
( ( leq(X,Y)
| ~ leq(s(X),s(Y)) )
& ( leq(s(X),s(Y))
| ~ leq(X,Y) ) ),
inference(fof_nnf,[status(thm)],[axiom_63]) ).
fof(f_64_2,plain,
! [U_170,U_169] :
( ( leq(U_170,U_169)
| ~ leq(s(U_170),s(U_169)) )
& ( leq(s(U_170),s(U_169))
| ~ leq(U_170,U_169) ) ),
inference(variable_rename,[status(thm)],[f_64_1]) ).
fof(f_64_3,plain,
( ! [U_174,U_172] :
( leq(U_174,U_172)
| ~ leq(s(U_174),s(U_172)) )
& ! [U_173,U_171] :
( leq(s(U_173),s(U_171))
| ~ leq(U_173,U_171) ) ),
inference(miniscope,[status(thm)],[f_64_2]) ).
cnf(f_64_4,plain,
( leq(s(U_173),s(U_171))
| ~ leq(U_173,U_171) ),
inference(clausify,[status(thm)],[f_64_3]) ).
cnf(f_64_5,plain,
( leq(U_174,U_172)
| ~ leq(s(U_174),s(U_172)) ),
inference(clausify,[status(thm)],[f_64_3]) ).
fof(f_65_1,plain,
! [X,Y] :
( ( leq(X,s(Y))
| ( ~ leq(X,Y)
& X != s(Y) ) )
& ( leq(X,Y)
| X = s(Y)
| ~ leq(X,s(Y)) ) ),
inference(fof_nnf,[status(thm)],[axiom_64]) ).
fof(f_65_2,plain,
! [U_176,U_175] :
( ( leq(U_176,s(U_175))
| ( ~ leq(U_176,U_175)
& U_176 != s(U_175) ) )
& ( leq(U_176,U_175)
| U_176 = s(U_175)
| ~ leq(U_176,s(U_175)) ) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
fof(f_65_3,plain,
( ! [U_180,U_178] :
( leq(U_180,s(U_178))
| ( ~ leq(U_180,U_178)
& U_180 != s(U_178) ) )
& ! [U_179,U_177] :
( leq(U_179,U_177)
| U_179 = s(U_177)
| ~ leq(U_179,s(U_177)) ) ),
inference(miniscope,[status(thm)],[f_65_2]) ).
cnf(f_65_4,plain,
( leq(U_179,U_177)
| U_179 = s(U_177)
| ~ leq(U_179,s(U_177)) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_5,plain,
( U_180 != s(U_178)
| leq(U_180,s(U_178)) ),
inference(clausify,[status(thm)],[f_65_3]) ).
cnf(f_65_6,plain,
( ~ leq(U_180,U_178)
| leq(U_180,s(U_178)) ),
inference(clausify,[status(thm)],[f_65_3]) ).
fof(f_66_1,plain,
! [X] : ~ setIn(X,setEmpty),
inference(fof_nnf,[status(thm)],[axiom_65]) ).
fof(f_66_2,plain,
! [U_181] : ~ setIn(U_181,setEmpty),
inference(variable_rename,[status(thm)],[f_66_1]) ).
cnf(f_66_3,plain,
~ setIn(U_181,setEmpty),
inference(clausify,[status(thm)],[f_66_2]) ).
fof(f_67_1,negated_conjecture,
~ ! [V,W,X,Y] :
( ( queue(host(X)) = cons(m_Ack(W,Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( ( host(Pid20) = s(index(pendack,host(Pid0)))
& host(Pid30) = index(pendack,host(Pid0))
& index(status,host(Pid0)) = elec_2
& leq(nbr_proc,s(index(pendack,host(Pid0))))
& elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid30,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& host(Pid0) = host(Pid30)
& host(Pid0) = nbr_proc
& elem(m_Down(Pid20),queue(host(Pid0)))
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( elem(m_Down(Pid30),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& elem(m_Halt(Pid0),queue(host(Pid20)))
& setIn(Pid0,alive)
& ~ leq(index(pendack,host(Pid0)),host(Z)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& host(Pid0) = host(Pid20)
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> ~ elem(m_Ack(Z,Pid20),queue(host(Z))) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& index(status,host(Z)) = elec_2
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Z),host(Pid0)) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Down(Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z] :
( ( setIn(Z,alive)
& ( index(status,host(Z)) = elec_2
| index(status,host(Z)) = elec_1 ) )
=> index(elid,host(Z)) = Z )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& setIn(Pid0,alive) )
=> ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
& ! [Z,Pid0] :
( ( elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> leq(host(Z),index(pendack,host(Pid0))) )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( elem(m_Ack(Pid0,Z),queue(host(Pid20)))
=> ~ leq(host(Z),host(Pid0)) )
& ! [Z,Pid0] :
( elem(m_Halt(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) )
& ! [Z,Pid0] :
( elem(m_Down(Pid0),queue(host(Z)))
=> host(Pid0) != host(Z) )
& ! [Z,Pid0] :
( elem(m_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( ( host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2
& index(elid,host(X)) = W )
=> ( leq(nbr_proc,index(pendack,host(X)))
=> ! [Z] :
( ( host(Z) = host(Y)
| setIn(host(Z),index(acks,host(X))) )
=> ! [V0] :
( host(X) != host(V0)
=> ! [W0,X0,Y0] :
( host(Z) = host(Y0)
=> ( host(X) != host(Y0)
=> ( ( host(X0) = s(index(pendack,host(Y0)))
& host(W0) = index(pendack,host(Y0))
& index(status,host(Y0)) = elec_2
& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
& leq(nbr_proc,s(index(pendack,host(Y0))))
& setIn(Y0,alive) )
=> ~ ( index(status,host(V0)) = norm
& index(ldr,host(V0)) = host(V0)
& setIn(V0,alive) ) ) ) ) ) ) ) ) ) ),
inference(negate,[status(cth)],[conj]) ).
fof(f_67_2,negated_conjecture,
? [V,W,X,Y] :
( ? [Z] :
( ? [V0] :
( ? [W0,X0,Y0] :
( index(status,host(V0)) = norm
& index(ldr,host(V0)) = host(V0)
& setIn(V0,alive)
& host(X0) = s(index(pendack,host(Y0)))
& host(W0) = index(pendack,host(Y0))
& index(status,host(Y0)) = elec_2
& elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
& elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
& leq(nbr_proc,s(index(pendack,host(Y0))))
& setIn(Y0,alive)
& host(X) != host(Y0)
& host(Z) = host(Y0) )
& host(X) != host(V0) )
& ( host(Z) = host(Y)
| setIn(host(Z),index(acks,host(X))) ) )
& leq(nbr_proc,index(pendack,host(X)))
& host(Y) = index(pendack,host(X))
& index(status,host(X)) = elec_2
& index(elid,host(X)) = W
& setIn(X,alive)
& queue(host(X)) = cons(m_Ack(W,Y),V)
& ! [Z,Pid30,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| host(Pid20) != s(index(pendack,host(Pid0)))
| host(Pid30) != index(pendack,host(Pid0))
| index(status,host(Pid0)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(Pid0))))
| ~ elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Z,Pid30,Pid20,Pid0] :
( ~ elem(m_Down(Pid30),queue(host(Z)))
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_1
| host(Pid0) != host(Pid30)
| host(Pid0) != nbr_proc
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ? [V0] :
( V0 != host(Pid20)
& ~ setIn(V0,index(down,host(Pid0)))
& leq(s(zero),V0)
& ~ leq(host(Pid0),V0) ) )
& ! [Z,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_2
| ~ elem(m_Halt(Pid0),queue(host(Pid20)))
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid0] :
( ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0)))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [Z,Pid20,Pid0] :
( ~ elem(m_Ack(Z,Pid20),queue(host(Z)))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| host(Pid0) != host(Pid20)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| index(status,host(Z)) != elec_2
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Z),host(Pid0)) )
& ! [Z,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| host(Pid20) != host(Z)
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Z] :
( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ! [Z,Pid0] :
( ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| index(status,host(Pid0)) != elec_1
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(host(Z),index(pendack,host(Pid0)))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid20,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid20))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Halt(Pid0),queue(host(Z))) )
& ! [Z,Pid0] :
( host(Pid0) != host(Z)
| ~ elem(m_Down(Pid0),queue(host(Z))) )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ldr(Pid0),queue(host(Z))) ) ),
inference(fof_nnf,[status(thm)],[f_67_1]) ).
fof(f_67_3,negated_conjecture,
? [U_228,U_227,U_226,U_225] :
( ? [U_224] :
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(U_226)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(U_226)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(U_226) != host(U_220)
& host(U_224) = host(U_220) )
& host(U_226) != host(U_223) )
& ( host(U_224) = host(U_225)
| setIn(host(U_224),index(acks,host(U_226))) ) )
& leq(nbr_proc,index(pendack,host(U_226)))
& host(U_225) = index(pendack,host(U_226))
& index(status,host(U_226)) = elec_2
& index(elid,host(U_226)) = U_227
& setIn(U_226,alive)
& queue(host(U_226)) = cons(m_Ack(U_227,U_225),U_228)
& ! [U_219,U_218,U_217,U_216] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive)
| host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) )
& ! [U_215,U_214,U_213,U_212] :
( ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive)
| index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ? [U_211] :
( U_211 != host(U_213)
& ~ setIn(U_211,index(down,host(U_212)))
& leq(s(zero),U_211)
& ~ leq(host(U_212),U_211) ) )
& ! [U_210,U_209,U_208] :
( index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive)
| index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204,U_203] :
( ~ elem(m_Ack(U_205,U_204),queue(host(U_205)))
| index(status,host(U_203)) != elec_2
| index(status,host(U_205)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive)
| ~ setIn(U_205,alive) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200,U_199,U_198] :
( index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive)
| host(U_199) != host(U_200)
| ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(variable_rename,[status(thm)],[f_67_2]) ).
fof(f_67_4,negated_conjecture,
? [U_228,U_227,U_226,U_225] :
( ? [U_224] :
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(U_226)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(U_226)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(U_226) != host(U_220)
& host(U_224) = host(U_220) )
& host(U_226) != host(U_223) )
& ( host(U_224) = host(U_225)
| setIn(host(U_224),index(acks,host(U_226))) ) )
& leq(nbr_proc,index(pendack,host(U_226)))
& host(U_225) = index(pendack,host(U_226))
& index(status,host(U_226)) = elec_2
& index(elid,host(U_226)) = U_227
& setIn(U_226,alive)
& queue(host(U_226)) = cons(m_Ack(U_227,U_225),U_228)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ? [U_211] :
( U_211 != host(U_213)
& ~ setIn(U_211,index(down,host(U_212)))
& leq(s(zero),U_211)
& ~ leq(host(U_212),U_211) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(miniscope,[status(thm)],[f_67_3]) ).
fof(f_67_5,negated_conjecture,
? [U_227,U_226,U_225] :
( ? [U_224] :
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(U_226)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(U_226)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(U_226) != host(U_220)
& host(U_224) = host(U_220) )
& host(U_226) != host(U_223) )
& ( host(U_224) = host(U_225)
| setIn(host(U_224),index(acks,host(U_226))) ) )
& leq(nbr_proc,index(pendack,host(U_226)))
& host(U_225) = index(pendack,host(U_226))
& index(status,host(U_226)) = elec_2
& index(elid,host(U_226)) = U_227
& setIn(U_226,alive)
& queue(host(U_226)) = cons(m_Ack(U_227,U_225),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ? [U_211] :
( U_211 != host(U_213)
& ~ setIn(U_211,index(down,host(U_212)))
& leq(s(zero),U_211)
& ~ leq(host(U_212),U_211) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_228,sK5)],[f_67_4]) ).
fof(f_67_6,negated_conjecture,
? [U_226,U_225] :
( ? [U_224] :
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(U_226)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(U_226)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(U_226) != host(U_220)
& host(U_224) = host(U_220) )
& host(U_226) != host(U_223) )
& ( host(U_224) = host(U_225)
| setIn(host(U_224),index(acks,host(U_226))) ) )
& leq(nbr_proc,index(pendack,host(U_226)))
& host(U_225) = index(pendack,host(U_226))
& index(status,host(U_226)) = elec_2
& index(elid,host(U_226)) = sK6
& setIn(U_226,alive)
& queue(host(U_226)) = cons(m_Ack(sK6,U_225),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ? [U_211] :
( U_211 != host(U_213)
& ~ setIn(U_211,index(down,host(U_212)))
& leq(s(zero),U_211)
& ~ leq(host(U_212),U_211) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_227,sK6)],[f_67_5]) ).
fof(f_67_7,negated_conjecture,
? [U_225] :
( ? [U_224] :
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(sK7)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(sK7) != host(U_220)
& host(U_224) = host(U_220) )
& host(sK7) != host(U_223) )
& ( host(U_224) = host(U_225)
| setIn(host(U_224),index(acks,host(sK7))) ) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(U_225) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,U_225),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ? [U_211] :
( U_211 != host(U_213)
& ~ setIn(U_211,index(down,host(U_212)))
& leq(s(zero),U_211)
& ~ leq(host(U_212),U_211) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_226,sK7)],[f_67_6]) ).
fof(f_67_8,negated_conjecture,
( ? [U_224] :
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(sK7)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(sK7) != host(U_220)
& host(U_224) = host(U_220) )
& host(sK7) != host(U_223) )
& ( host(U_224) = host(sK8)
| setIn(host(U_224),index(acks,host(sK7))) ) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ? [U_211] :
( U_211 != host(U_213)
& ~ setIn(U_211,index(down,host(U_212)))
& leq(s(zero),U_211)
& ~ leq(host(U_212),U_211) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_225,sK8)],[f_67_7]) ).
fof(f_67_9,negated_conjecture,
( ? [U_224] :
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(sK7)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(sK7) != host(U_220)
& host(U_224) = host(U_220) )
& host(sK7) != host(U_223) )
& ( host(U_224) = host(sK8)
| setIn(host(U_224),index(acks,host(sK7))) ) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ( sK9(U_215,U_214,U_213,U_212) != host(U_213)
& ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
& leq(s(zero),sK9(U_215,U_214,U_213,U_212))
& ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212)) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_211,sK9(U_215,U_214,U_213,U_212))],[f_67_8]) ).
fof(f_67_10,negated_conjecture,
( ? [U_223] :
( ? [U_222,U_221,U_220] :
( index(status,host(U_223)) = norm
& index(ldr,host(U_223)) = host(U_223)
& setIn(U_223,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(sK7)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(sK7) != host(U_220)
& host(sK10) = host(U_220) )
& host(sK7) != host(U_223) )
& ( host(sK10) = host(sK8)
| setIn(host(sK10),index(acks,host(sK7))) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ( sK9(U_215,U_214,U_213,U_212) != host(U_213)
& ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
& leq(s(zero),sK9(U_215,U_214,U_213,U_212))
& ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212)) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_224,sK10)],[f_67_9]) ).
fof(f_67_11,negated_conjecture,
( ? [U_222,U_221,U_220] :
( index(status,host(sK11)) = norm
& index(ldr,host(sK11)) = host(sK11)
& setIn(sK11,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(U_222) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,U_222),snoc(queue(host(U_220)),m_Ldr(sK7)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(sK7) != host(U_220)
& host(sK10) = host(U_220) )
& host(sK7) != host(sK11)
& ( host(sK10) = host(sK8)
| setIn(host(sK10),index(acks,host(sK7))) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ( sK9(U_215,U_214,U_213,U_212) != host(U_213)
& ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
& leq(s(zero),sK9(U_215,U_214,U_213,U_212))
& ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212)) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_223,sK11)],[f_67_10]) ).
fof(f_67_12,negated_conjecture,
( ? [U_221,U_220] :
( index(status,host(sK11)) = norm
& index(ldr,host(sK11)) = host(sK11)
& setIn(sK11,alive)
& host(U_221) = s(index(pendack,host(U_220)))
& host(sK12) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,sK12),snoc(queue(host(U_220)),m_Ldr(sK7)))
& elem(m_Down(U_221),snoc(queue(host(U_220)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(sK7) != host(U_220)
& host(sK10) = host(U_220) )
& host(sK7) != host(sK11)
& ( host(sK10) = host(sK8)
| setIn(host(sK10),index(acks,host(sK7))) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ( sK9(U_215,U_214,U_213,U_212) != host(U_213)
& ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
& leq(s(zero),sK9(U_215,U_214,U_213,U_212))
& ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212)) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_222,sK12)],[f_67_11]) ).
fof(f_67_13,negated_conjecture,
( ? [U_220] :
( index(status,host(sK11)) = norm
& index(ldr,host(sK11)) = host(sK11)
& setIn(sK11,alive)
& host(sK13) = s(index(pendack,host(U_220)))
& host(sK12) = index(pendack,host(U_220))
& index(status,host(U_220)) = elec_2
& elem(m_Ack(U_220,sK12),snoc(queue(host(U_220)),m_Ldr(sK7)))
& elem(m_Down(sK13),snoc(queue(host(U_220)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(U_220))))
& setIn(U_220,alive)
& host(sK7) != host(U_220)
& host(sK10) = host(U_220) )
& host(sK7) != host(sK11)
& ( host(sK10) = host(sK8)
| setIn(host(sK10),index(acks,host(sK7))) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ( sK9(U_215,U_214,U_213,U_212) != host(U_213)
& ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
& leq(s(zero),sK9(U_215,U_214,U_213,U_212))
& ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212)) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_221,sK13)],[f_67_12]) ).
fof(f_67_14,negated_conjecture,
( index(status,host(sK11)) = norm
& index(ldr,host(sK11)) = host(sK11)
& setIn(sK11,alive)
& host(sK13) = s(index(pendack,host(sK14)))
& host(sK12) = index(pendack,host(sK14))
& index(status,host(sK14)) = elec_2
& elem(m_Ack(sK14,sK12),snoc(queue(host(sK14)),m_Ldr(sK7)))
& elem(m_Down(sK13),snoc(queue(host(sK14)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(sK14))))
& setIn(sK14,alive)
& host(sK7) != host(sK14)
& host(sK10) = host(sK14)
& host(sK7) != host(sK11)
& ( host(sK10) = host(sK8)
| setIn(host(sK10),index(acks,host(sK7))) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ( ! [U_219] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive) )
| ! [U_218,U_217,U_216] :
( host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ) )
& ! [U_215,U_214] :
( ! [U_213,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| ( sK9(U_215,U_214,U_213,U_212) != host(U_213)
& ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
& leq(s(zero),sK9(U_215,U_214,U_213,U_212))
& ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212)) ) )
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_210] :
( ! [U_209,U_208] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210)) )
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_207,U_206] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_204] :
( ! [U_203] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive) )
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_202,U_201] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_200] :
( ! [U_199] :
( ! [U_198] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive) )
| host(U_199) != host(U_200) )
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| ( index(status,host(U_197)) != elec_2
& index(status,host(U_197)) != elec_1 ) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_194,U_193] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_190,U_189,U_188] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_187,U_186] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_183,U_182] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_220,sK14)],[f_67_13]) ).
fof(f_67_15,negated_conjecture,
( ! [U_213,U_214,U_215,U_212] :
( sK9(U_215,U_214,U_213,U_212) != host(U_213)
| ~ sP1(U_213,U_214,U_215,U_212) )
& ! [U_213,U_214,U_215,U_212] :
( ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
| ~ sP1(U_213,U_214,U_215,U_212) )
& ! [U_213,U_214,U_215,U_212] :
( leq(s(zero),sK9(U_215,U_214,U_213,U_212))
| ~ sP1(U_213,U_214,U_215,U_212) )
& ! [U_213,U_214,U_215,U_212] :
( ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212))
| ~ sP1(U_213,U_214,U_215,U_212) )
& ! [U_197] :
( index(status,host(U_197)) != elec_2
| ~ sP0(U_197) )
& ! [U_197] :
( index(status,host(U_197)) != elec_1
| ~ sP0(U_197) )
& index(status,host(sK11)) = norm
& index(ldr,host(sK11)) = host(sK11)
& setIn(sK11,alive)
& host(sK13) = s(index(pendack,host(sK14)))
& host(sK12) = index(pendack,host(sK14))
& index(status,host(sK14)) = elec_2
& elem(m_Ack(sK14,sK12),snoc(queue(host(sK14)),m_Ldr(sK7)))
& elem(m_Down(sK13),snoc(queue(host(sK14)),m_Ldr(sK7)))
& leq(nbr_proc,s(index(pendack,host(sK14))))
& setIn(sK14,alive)
& host(sK7) != host(sK14)
& host(sK10) = host(sK14)
& host(sK7) != host(sK11)
& ( host(sK10) = host(sK8)
| setIn(host(sK10),index(acks,host(sK7))) )
& leq(nbr_proc,index(pendack,host(sK7)))
& host(sK8) = index(pendack,host(sK7))
& index(status,host(sK7)) = elec_2
& index(elid,host(sK7)) = sK6
& setIn(sK7,alive)
& queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5)
& ! [U_217,U_218,U_219,U_216] :
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive)
| host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) )
& ! [U_213,U_214,U_215,U_212] :
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| sP1(U_213,U_214,U_215,U_212)
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) )
& ! [U_209,U_208,U_210] :
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210))
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) )
& ! [U_206,U_207] :
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) )
& ! [U_205,U_203,U_204] :
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive)
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) )
& ! [U_201,U_202] :
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) )
& ! [U_199,U_198,U_200] :
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive)
| host(U_199) != host(U_200)
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) )
& ! [U_197] :
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| sP0(U_197) )
& ! [U_196,U_195] :
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) )
& ! [U_193,U_194] :
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) )
& ! [U_192,U_191] :
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 )
& ! [U_188,U_190,U_189] :
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) )
& ! [U_186,U_187] :
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) )
& ! [U_185,U_184] :
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) )
& ! [U_182,U_183] :
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_67_14]) ).
cnf(f_67_16,negated_conjecture,
( ~ leq(host(U_183),host(U_182))
| ~ elem(m_Ldr(U_182),queue(host(U_183))) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_17,negated_conjecture,
( host(U_184) != host(U_185)
| ~ elem(m_Down(U_184),queue(host(U_185))) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_18,negated_conjecture,
( ~ leq(host(U_187),host(U_186))
| ~ elem(m_Halt(U_186),queue(host(U_187))) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_19,negated_conjecture,
( ~ leq(host(U_190),host(U_188))
| ~ elem(m_Ack(U_188,U_190),queue(host(U_189))) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_20,negated_conjecture,
( ~ setIn(U_191,alive)
| ~ setIn(U_192,alive)
| host(U_191) != host(U_192)
| U_191 = U_192 ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_21,negated_conjecture,
( leq(host(U_194),index(pendack,host(U_193)))
| ~ elem(m_Ack(U_193,U_194),queue(host(U_193)))
| ~ setIn(U_193,alive) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_22,negated_conjecture,
( ~ elem(m_Ack(U_195,U_196),queue(host(U_195)))
| index(status,host(U_195)) != elec_1
| ~ setIn(U_195,alive) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_23,negated_conjecture,
( index(elid,host(U_197)) = U_197
| ~ setIn(U_197,alive)
| sP0(U_197) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_24,negated_conjecture,
( ~ elem(m_Down(U_199),queue(host(U_198)))
| ~ setIn(U_198,alive)
| host(U_199) != host(U_200)
| index(status,host(U_200)) != norm
| index(ldr,host(U_200)) != host(U_200)
| ~ setIn(U_200,alive) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_25,negated_conjecture,
( leq(index(pendack,host(U_201)),host(U_202))
| index(status,host(U_201)) != elec_2
| index(status,host(U_202)) != elec_2
| ~ setIn(U_201,alive)
| ~ setIn(U_202,alive)
| leq(host(U_202),host(U_201)) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_26,negated_conjecture,
( index(status,host(U_203)) != elec_2
| host(U_203) != host(U_204)
| ~ setIn(U_203,alive)
| index(status,host(U_205)) != elec_2
| ~ setIn(U_205,alive)
| ~ elem(m_Ack(U_205,U_204),queue(host(U_205))) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_27,negated_conjecture,
( ~ leq(index(pendack,host(U_207)),index(pendack,host(U_206)))
| index(status,host(U_206)) != elec_2
| index(status,host(U_207)) != elec_2
| ~ setIn(U_206,alive)
| ~ setIn(U_207,alive)
| leq(host(U_207),host(U_206)) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_28,negated_conjecture,
( index(status,host(U_208)) != elec_2
| ~ elem(m_Halt(U_208),queue(host(U_209)))
| ~ setIn(U_208,alive)
| leq(index(pendack,host(U_208)),host(U_210))
| index(status,host(U_210)) != norm
| index(ldr,host(U_210)) != host(U_210)
| ~ setIn(U_210,alive) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_29,negated_conjecture,
( index(status,host(U_212)) != elec_1
| host(U_212) != host(U_214)
| host(U_212) != nbr_proc
| ~ elem(m_Down(U_213),queue(host(U_212)))
| sP1(U_213,U_214,U_215,U_212)
| ~ elem(m_Down(U_214),queue(host(U_215)))
| ~ setIn(U_215,alive) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_30,negated_conjecture,
( index(status,host(U_219)) != norm
| index(ldr,host(U_219)) != host(U_219)
| ~ setIn(U_219,alive)
| host(U_217) != s(index(pendack,host(U_216)))
| host(U_218) != index(pendack,host(U_216))
| index(status,host(U_216)) != elec_2
| ~ leq(nbr_proc,s(index(pendack,host(U_216))))
| ~ elem(m_Ack(U_216,U_218),queue(host(U_216)))
| ~ elem(m_Down(U_217),queue(host(U_216)))
| ~ setIn(U_216,alive) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_31,negated_conjecture,
queue(host(sK7)) = cons(m_Ack(sK6,sK8),sK5),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_32,negated_conjecture,
setIn(sK7,alive),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_33,negated_conjecture,
index(elid,host(sK7)) = sK6,
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_34,negated_conjecture,
index(status,host(sK7)) = elec_2,
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_35,negated_conjecture,
host(sK8) = index(pendack,host(sK7)),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_36,negated_conjecture,
leq(nbr_proc,index(pendack,host(sK7))),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_37,negated_conjecture,
( host(sK10) = host(sK8)
| setIn(host(sK10),index(acks,host(sK7))) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_38,negated_conjecture,
host(sK7) != host(sK11),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_39,negated_conjecture,
host(sK10) = host(sK14),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_40,negated_conjecture,
host(sK7) != host(sK14),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_41,negated_conjecture,
setIn(sK14,alive),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_42,negated_conjecture,
leq(nbr_proc,s(index(pendack,host(sK14)))),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_43,negated_conjecture,
elem(m_Down(sK13),snoc(queue(host(sK14)),m_Ldr(sK7))),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_44,negated_conjecture,
elem(m_Ack(sK14,sK12),snoc(queue(host(sK14)),m_Ldr(sK7))),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_45,negated_conjecture,
index(status,host(sK14)) = elec_2,
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_46,negated_conjecture,
host(sK12) = index(pendack,host(sK14)),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_47,negated_conjecture,
host(sK13) = s(index(pendack,host(sK14))),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_48,negated_conjecture,
setIn(sK11,alive),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_49,negated_conjecture,
index(ldr,host(sK11)) = host(sK11),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_50,negated_conjecture,
index(status,host(sK11)) = norm,
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_51,negated_conjecture,
( index(status,host(U_197)) != elec_1
| ~ sP0(U_197) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_52,negated_conjecture,
( index(status,host(U_197)) != elec_2
| ~ sP0(U_197) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_53,negated_conjecture,
( ~ leq(host(U_212),sK9(U_215,U_214,U_213,U_212))
| ~ sP1(U_213,U_214,U_215,U_212) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_54,negated_conjecture,
( leq(s(zero),sK9(U_215,U_214,U_213,U_212))
| ~ sP1(U_213,U_214,U_215,U_212) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_55,negated_conjecture,
( ~ setIn(sK9(U_215,U_214,U_213,U_212),index(down,host(U_212)))
| ~ sP1(U_213,U_214,U_215,U_212) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(f_67_56,negated_conjecture,
( sK9(U_215,U_214,U_213,U_212) != host(U_213)
| ~ sP1(U_213,U_214,U_215,U_212) ),
inference(clausify,[status(thm)],[f_67_15]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( m_Ack(Eq_x_0,Eq_x_1) = m_Ack(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( host(Eq_x_0) = host(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( queue(Eq_x_0) = queue(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( s(Eq_x_0) = s(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( m_Halt(Eq_x_0) = m_Halt(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( m_Down(Eq_x_0) = m_Down(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( m_NotNorm(Eq_x_0) = m_NotNorm(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( m_Ldr(Eq_x_0) = m_Ldr(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( m_NormQ(Eq_x_0) = m_NormQ(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( cons(Eq_x_0,Eq_x_1) = cons(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( head(Eq_x_0) = head(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( tail(Eq_x_0) = tail(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( snoc(Eq_x_0,Eq_x_1) = snoc(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( last(Eq_x_0) = last(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( init(Eq_x_0) = init(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( pidMsg(Eq_x_0) = pidMsg(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( index(Eq_x_0,Eq_x_1) = index(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( sK1(Eq_x_0) = sK1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( sK2(Eq_x_0) = sK2(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( sK3(Eq_x_0,Eq_x_1) = sK3(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( sK4(Eq_x_0,Eq_x_1) = sK4(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( sK9(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK9(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( elem(Eq_y_0,Eq_y_1)
| ~ elem(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( setIn(Eq_y_0,Eq_y_1)
| ~ setIn(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( leq(Eq_y_0,Eq_y_1)
| ~ leq(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( pidElem(Eq_y_0)
| ~ pidElem(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( ordered(Eq_y_0)
| ~ ordered(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( sP0(Eq_y_0)
| ~ sP0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,axiom,
( sP1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV463+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n009.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sun Sep 20 03:42:32 UTC 2026
% 0.11/5.38 % CPUTime :
% 11.05/16.33 % SZS status Theorem for theBenchmark
% 11.05/16.33 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------