%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV457+1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:23:19 PM UTC 2026
% Result : Theorem 8.34s 5.76s
% Output : CNFRefutation 8.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 65 ( 32 unt; 0 def)
% Number of atoms : 432 ( 166 equ)
% Maximal formula atoms : 79 ( 6 avg)
% Number of connectives : 561 ( 194 ~; 130 |; 173 &)
% ( 4 <=>; 60 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 17 con; 0-2 aty)
% Number of variables : 255 ( 34 sgn 193 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conj,conjecture,
! [X12,X13,X5] :
( ( ! [X6,X7] :
( elem(m_Ack(X7,X6),queue(host(X7)))
=> setIn(X7,pids) )
& ! [X6,X7] :
( elem(m_Down(X7),queue(host(X6)))
=> ~ setIn(X7,alive) )
& ! [X6,X7] :
( elem(m_Ldr(X7),queue(host(X6)))
=> ~ leq(host(X6),host(X7)) )
& ! [X6,X7,X14] :
( elem(m_Ack(X14,X6),queue(host(X7)))
=> ~ leq(host(X6),host(X14)) )
& ! [X6,X7] :
( ( ~ setIn(X6,alive)
& leq(X7,X6)
& host(X7) = host(X6) )
=> ~ setIn(X7,alive) )
& ! [X6,X7] :
( ( X7 != X6
& host(X7) = host(X6) )
=> ( ~ setIn(X6,alive)
| ~ setIn(X7,alive) ) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& elem(m_Ack(X7,X6),queue(host(X7))) )
=> leq(host(X6),index(pendack,host(X7))) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& index(status,host(X7)) = elec_1 )
=> ~ elem(m_Ack(X6,X7),queue(host(X6))) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& index(status,host(X7)) = elec_1 )
=> ~ elem(m_Ack(X7,X6),queue(host(X7))) )
& ! [X6] :
( ( ( index(status,host(X6)) = elec_1
| index(status,host(X6)) = elec_2 )
& setIn(X6,alive) )
=> index(elid,host(X6)) = X6 )
& ! [X6,X7,X14] :
( ( elem(m_Down(X6),queue(host(X7)))
& elem(m_Ack(X14,X7),queue(host(X14)))
& host(X14) = host(X6) )
=> ~ setIn(X14,alive) )
& ! [X6,X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& elem(m_Ack(X14,X6),queue(host(X14)))
& host(X7) = host(X6) )
=> ~ setIn(host(X14),index(down,host(X7))) )
& ! [X6,X7] :
( ( ~ leq(host(X6),host(X7))
& setIn(X6,alive)
& setIn(X7,alive)
& index(status,host(X6)) = elec_2
& index(status,host(X7)) = elec_2 )
=> ~ leq(index(pendack,host(X6)),index(pendack,host(X7))) )
& ! [X6,X7,X14] :
( ( ~ leq(index(pendack,host(X14)),host(X6))
& setIn(X14,alive)
& elem(m_Halt(X14),queue(host(X7)))
& index(status,host(X14)) = elec_2 )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) )
& ! [X6,X7,X14] :
( ( setIn(X14,alive)
& elem(m_Ack(X14,X7),queue(host(X14)))
& leq(nbr_proc,index(pendack,host(X14)))
& index(status,host(X14)) = elec_2
& host(X7) = index(pendack,host(X14)) )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) )
& queue(host(X13)) = cons(m_Halt(X5),X12) )
=> ( setIn(X13,alive)
=> ! [X6] :
( host(X13) != host(X6)
=> ! [X7,X15] :
( host(X5) = host(X15)
=> ( host(X13) != host(X15)
=> ( ( setIn(X15,alive)
& leq(nbr_proc,index(pendack,host(X15)))
& elem(m_Ack(X15,X7),snoc(queue(host(X15)),m_Ack(X5,X13)))
& index(status,host(X15)) = elec_2
& host(X7) = index(pendack,host(X15)) )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
fof(axiom_61,axiom,
! [X5,X6] :
( ( leq(X5,X6)
& leq(X6,X5) )
<=> X5 = X6 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_61) ).
fof(axiom_04,axiom,
! [X3] : leq(host(X3),nbr_proc),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_04) ).
fof(axiom_59,axiom,
! [X5] : leq(X5,X5),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_59) ).
fof(axiom_47,axiom,
! [X5,X6,X4] :
( elem(X5,snoc(X4,X6))
<=> ( X5 = X6
| elem(X5,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_47) ).
fof(axiom_31,axiom,
! [X8,X9,X10,X11] :
( X8 != X9
=> m_Ack(X8,X10) != m_Ack(X9,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_31) ).
fof(axiom_46,axiom,
! [X5,X6,X4] :
( elem(X5,cons(X6,X4))
<=> ( X5 = X6
| elem(X5,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_46) ).
fof(axiom_32,axiom,
! [X8,X9,X10,X11] :
( X10 != X11
=> m_Ack(X8,X10) != m_Ack(X9,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV011+0.ax',axiom_32) ).
fof(c_0_8,plain,
! [X13,X5,X12] :
( epred1_3(X12,X5,X13)
<=> ( ! [X6,X7] :
( elem(m_Ack(X7,X6),queue(host(X7)))
=> setIn(X7,pids) )
& ! [X6,X7] :
( elem(m_Down(X7),queue(host(X6)))
=> ~ setIn(X7,alive) )
& ! [X6,X7] :
( elem(m_Ldr(X7),queue(host(X6)))
=> ~ leq(host(X6),host(X7)) )
& ! [X6,X7,X14] :
( elem(m_Ack(X14,X6),queue(host(X7)))
=> ~ leq(host(X6),host(X14)) )
& ! [X6,X7] :
( ( ~ setIn(X6,alive)
& leq(X7,X6)
& host(X7) = host(X6) )
=> ~ setIn(X7,alive) )
& ! [X6,X7] :
( ( X7 != X6
& host(X7) = host(X6) )
=> ( ~ setIn(X6,alive)
| ~ setIn(X7,alive) ) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& elem(m_Ack(X7,X6),queue(host(X7))) )
=> leq(host(X6),index(pendack,host(X7))) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& index(status,host(X7)) = elec_1 )
=> ~ elem(m_Ack(X6,X7),queue(host(X6))) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& index(status,host(X7)) = elec_1 )
=> ~ elem(m_Ack(X7,X6),queue(host(X7))) )
& ! [X6] :
( ( ( index(status,host(X6)) = elec_1
| index(status,host(X6)) = elec_2 )
& setIn(X6,alive) )
=> index(elid,host(X6)) = X6 )
& ! [X6,X7,X14] :
( ( elem(m_Down(X6),queue(host(X7)))
& elem(m_Ack(X14,X7),queue(host(X14)))
& host(X14) = host(X6) )
=> ~ setIn(X14,alive) )
& ! [X6,X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& elem(m_Ack(X14,X6),queue(host(X14)))
& host(X7) = host(X6) )
=> ~ setIn(host(X14),index(down,host(X7))) )
& ! [X6,X7] :
( ( ~ leq(host(X6),host(X7))
& setIn(X6,alive)
& setIn(X7,alive)
& index(status,host(X6)) = elec_2
& index(status,host(X7)) = elec_2 )
=> ~ leq(index(pendack,host(X6)),index(pendack,host(X7))) )
& ! [X6,X7,X14] :
( ( ~ leq(index(pendack,host(X14)),host(X6))
& setIn(X14,alive)
& elem(m_Halt(X14),queue(host(X7)))
& index(status,host(X14)) = elec_2 )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) )
& ! [X6,X7,X14] :
( ( setIn(X14,alive)
& elem(m_Ack(X14,X7),queue(host(X14)))
& leq(nbr_proc,index(pendack,host(X14)))
& index(status,host(X14)) = elec_2
& host(X7) = index(pendack,host(X14)) )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) )
& queue(host(X13)) = cons(m_Halt(X5),X12) ) ),
introduced(definition) ).
fof(c_0_9,negated_conjecture,
~ ! [X12,X13,X5] :
( epred1_3(X12,X5,X13)
=> ( setIn(X13,alive)
=> ! [X6] :
( host(X13) != host(X6)
=> ! [X7,X15] :
( host(X5) = host(X15)
=> ( host(X13) != host(X15)
=> ( ( setIn(X15,alive)
& leq(nbr_proc,index(pendack,host(X15)))
& elem(m_Ack(X15,X7),snoc(queue(host(X15)),m_Ack(X5,X13)))
& index(status,host(X15)) = elec_2
& host(X7) = index(pendack,host(X15)) )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) ) ) ) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[conj])]),c_0_8]) ).
fof(c_0_10,negated_conjecture,
( epred1_3(esk5_0,esk7_0,esk6_0)
& setIn(esk6_0,alive)
& host(esk6_0) != host(esk8_0)
& host(esk7_0) = host(esk10_0)
& host(esk6_0) != host(esk10_0)
& setIn(esk10_0,alive)
& leq(nbr_proc,index(pendack,host(esk10_0)))
& elem(m_Ack(esk10_0,esk9_0),snoc(queue(host(esk10_0)),m_Ack(esk7_0,esk6_0)))
& index(status,host(esk10_0)) = elec_2
& host(esk9_0) = index(pendack,host(esk10_0))
& setIn(esk8_0,alive)
& index(ldr,host(esk8_0)) = host(esk8_0)
& index(status,host(esk8_0)) = norm ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])]) ).
fof(c_0_11,plain,
! [X294,X295] :
( ( ~ leq(X294,X295)
| ~ leq(X295,X294)
| X294 = X295 )
& ( leq(X294,X295)
| X294 != X295 )
& ( leq(X295,X294)
| X294 != X295 ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_61])])]) ).
cnf(c_0_12,negated_conjecture,
leq(nbr_proc,index(pendack,host(esk10_0))),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_13,negated_conjecture,
host(esk9_0) = index(pendack,host(esk10_0)),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
fof(c_0_14,plain,
! [X180] : leq(host(X180),nbr_proc),
inference(variable_rename,[status(thm)],[axiom_04]) ).
fof(c_0_15,plain,
! [X13,X5,X12] :
( epred1_3(X12,X5,X13)
=> ( ! [X6,X7] :
( elem(m_Ack(X7,X6),queue(host(X7)))
=> setIn(X7,pids) )
& ! [X6,X7] :
( elem(m_Down(X7),queue(host(X6)))
=> ~ setIn(X7,alive) )
& ! [X6,X7] :
( elem(m_Ldr(X7),queue(host(X6)))
=> ~ leq(host(X6),host(X7)) )
& ! [X6,X7,X14] :
( elem(m_Ack(X14,X6),queue(host(X7)))
=> ~ leq(host(X6),host(X14)) )
& ! [X6,X7] :
( ( ~ setIn(X6,alive)
& leq(X7,X6)
& host(X7) = host(X6) )
=> ~ setIn(X7,alive) )
& ! [X6,X7] :
( ( X7 != X6
& host(X7) = host(X6) )
=> ( ~ setIn(X6,alive)
| ~ setIn(X7,alive) ) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& elem(m_Ack(X7,X6),queue(host(X7))) )
=> leq(host(X6),index(pendack,host(X7))) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& index(status,host(X7)) = elec_1 )
=> ~ elem(m_Ack(X6,X7),queue(host(X6))) )
& ! [X6,X7] :
( ( setIn(X7,alive)
& index(status,host(X7)) = elec_1 )
=> ~ elem(m_Ack(X7,X6),queue(host(X7))) )
& ! [X6] :
( ( ( index(status,host(X6)) = elec_1
| index(status,host(X6)) = elec_2 )
& setIn(X6,alive) )
=> index(elid,host(X6)) = X6 )
& ! [X6,X7,X14] :
( ( elem(m_Down(X6),queue(host(X7)))
& elem(m_Ack(X14,X7),queue(host(X14)))
& host(X14) = host(X6) )
=> ~ setIn(X14,alive) )
& ! [X6,X7,X14] :
( ( setIn(X7,alive)
& setIn(X14,alive)
& elem(m_Ack(X14,X6),queue(host(X14)))
& host(X7) = host(X6) )
=> ~ setIn(host(X14),index(down,host(X7))) )
& ! [X6,X7] :
( ( ~ leq(host(X6),host(X7))
& setIn(X6,alive)
& setIn(X7,alive)
& index(status,host(X6)) = elec_2
& index(status,host(X7)) = elec_2 )
=> ~ leq(index(pendack,host(X6)),index(pendack,host(X7))) )
& ! [X6,X7,X14] :
( ( ~ leq(index(pendack,host(X14)),host(X6))
& setIn(X14,alive)
& elem(m_Halt(X14),queue(host(X7)))
& index(status,host(X14)) = elec_2 )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) )
& ! [X6,X7,X14] :
( ( setIn(X14,alive)
& elem(m_Ack(X14,X7),queue(host(X14)))
& leq(nbr_proc,index(pendack,host(X14)))
& index(status,host(X14)) = elec_2
& host(X7) = index(pendack,host(X14)) )
=> ~ ( setIn(X6,alive)
& index(ldr,host(X6)) = host(X6)
& index(status,host(X6)) = norm ) )
& queue(host(X13)) = cons(m_Halt(X5),X12) ) ),
inference(split_equiv,[status(thm)],[c_0_8]) ).
cnf(c_0_16,plain,
( X1 = X2
| ~ leq(X1,X2)
| ~ leq(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_17,negated_conjecture,
leq(nbr_proc,host(esk9_0)),
inference(rw,[status(thm)],[c_0_12,c_0_13]) ).
cnf(c_0_18,plain,
leq(host(X1),nbr_proc),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
fof(c_0_19,plain,
! [X310,X311,X312,X313,X314,X315,X316,X317,X318,X319,X320,X321,X322,X323,X324,X325,X326,X327,X328,X329,X330,X331,X332,X333,X334,X335,X336,X337,X338,X339,X340,X341,X342,X343,X344,X345,X346] :
( ( ~ elem(m_Ack(X314,X313),queue(host(X314)))
| setIn(X314,pids)
| ~ epred1_3(X312,X311,X310) )
& ( ~ elem(m_Down(X316),queue(host(X315)))
| ~ setIn(X316,alive)
| ~ epred1_3(X312,X311,X310) )
& ( ~ elem(m_Ldr(X318),queue(host(X317)))
| ~ leq(host(X317),host(X318))
| ~ epred1_3(X312,X311,X310) )
& ( ~ elem(m_Ack(X321,X319),queue(host(X320)))
| ~ leq(host(X319),host(X321))
| ~ epred1_3(X312,X311,X310) )
& ( setIn(X322,alive)
| ~ leq(X323,X322)
| host(X323) != host(X322)
| ~ setIn(X323,alive)
| ~ epred1_3(X312,X311,X310) )
& ( X325 = X324
| host(X325) != host(X324)
| ~ setIn(X324,alive)
| ~ setIn(X325,alive)
| ~ epred1_3(X312,X311,X310) )
& ( ~ setIn(X327,alive)
| ~ elem(m_Ack(X327,X326),queue(host(X327)))
| leq(host(X326),index(pendack,host(X327)))
| ~ epred1_3(X312,X311,X310) )
& ( ~ setIn(X329,alive)
| index(status,host(X329)) != elec_1
| ~ elem(m_Ack(X328,X329),queue(host(X328)))
| ~ epred1_3(X312,X311,X310) )
& ( ~ setIn(X331,alive)
| index(status,host(X331)) != elec_1
| ~ elem(m_Ack(X331,X330),queue(host(X331)))
| ~ epred1_3(X312,X311,X310) )
& ( index(status,host(X332)) != elec_1
| ~ setIn(X332,alive)
| index(elid,host(X332)) = X332
| ~ epred1_3(X312,X311,X310) )
& ( index(status,host(X332)) != elec_2
| ~ setIn(X332,alive)
| index(elid,host(X332)) = X332
| ~ epred1_3(X312,X311,X310) )
& ( ~ elem(m_Down(X333),queue(host(X334)))
| ~ elem(m_Ack(X335,X334),queue(host(X335)))
| host(X335) != host(X333)
| ~ setIn(X335,alive)
| ~ epred1_3(X312,X311,X310) )
& ( ~ setIn(X337,alive)
| ~ setIn(X338,alive)
| ~ elem(m_Ack(X338,X336),queue(host(X338)))
| host(X337) != host(X336)
| ~ setIn(host(X338),index(down,host(X337)))
| ~ epred1_3(X312,X311,X310) )
& ( leq(host(X339),host(X340))
| ~ setIn(X339,alive)
| ~ setIn(X340,alive)
| index(status,host(X339)) != elec_2
| index(status,host(X340)) != elec_2
| ~ leq(index(pendack,host(X339)),index(pendack,host(X340)))
| ~ epred1_3(X312,X311,X310) )
& ( leq(index(pendack,host(X343)),host(X341))
| ~ setIn(X343,alive)
| ~ elem(m_Halt(X343),queue(host(X342)))
| index(status,host(X343)) != elec_2
| ~ setIn(X341,alive)
| index(ldr,host(X341)) != host(X341)
| index(status,host(X341)) != norm
| ~ epred1_3(X312,X311,X310) )
& ( ~ setIn(X346,alive)
| ~ elem(m_Ack(X346,X345),queue(host(X346)))
| ~ leq(nbr_proc,index(pendack,host(X346)))
| index(status,host(X346)) != elec_2
| host(X345) != index(pendack,host(X346))
| ~ setIn(X344,alive)
| index(ldr,host(X344)) != host(X344)
| index(status,host(X344)) != norm
| ~ epred1_3(X312,X311,X310) )
& ( queue(host(X310)) = cons(m_Halt(X311),X312)
| ~ epred1_3(X312,X311,X310) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_15])])])]) ).
cnf(c_0_20,negated_conjecture,
host(esk9_0) = nbr_proc,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16,c_0_17]),c_0_18])]) ).
fof(c_0_21,plain,
! [X291] : leq(X291,X291),
inference(variable_rename,[status(thm)],[axiom_59]) ).
fof(c_0_22,plain,
! [X258,X259,X260] :
( ( ~ elem(X258,snoc(X260,X259))
| X258 = X259
| elem(X258,X260) )
& ( X258 != X259
| elem(X258,snoc(X260,X259)) )
& ( ~ elem(X258,X260)
| elem(X258,snoc(X260,X259)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_47])])]) ).
cnf(c_0_23,plain,
( ~ setIn(X1,alive)
| ~ elem(m_Ack(X1,X2),queue(host(X1)))
| ~ leq(nbr_proc,index(pendack,host(X1)))
| index(status,host(X1)) != elec_2
| host(X2) != index(pendack,host(X1))
| ~ setIn(X3,alive)
| index(ldr,host(X3)) != host(X3)
| index(status,host(X3)) != norm
| ~ epred1_3(X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_24,negated_conjecture,
index(pendack,host(esk10_0)) = nbr_proc,
inference(rw,[status(thm)],[c_0_13,c_0_20]) ).
cnf(c_0_25,negated_conjecture,
index(status,host(esk10_0)) = elec_2,
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_26,plain,
leq(X1,X1),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_27,negated_conjecture,
setIn(esk10_0,alive),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_28,plain,
( X1 = X3
| elem(X1,X2)
| ~ elem(X1,snoc(X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_29,negated_conjecture,
elem(m_Ack(esk10_0,esk9_0),snoc(queue(host(esk10_0)),m_Ack(esk7_0,esk6_0))),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_30,negated_conjecture,
( index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm
| host(X2) != nbr_proc
| ~ epred1_3(X3,X4,X5)
| ~ setIn(X1,alive)
| ~ elem(m_Ack(esk10_0,X2),queue(host(esk10_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_24]),c_0_25]),c_0_26]),c_0_27])]) ).
cnf(c_0_31,negated_conjecture,
( m_Ack(esk7_0,esk6_0) = m_Ack(esk10_0,esk9_0)
| elem(m_Ack(esk10_0,esk9_0),queue(host(esk10_0))) ),
inference(spm,[status(thm)],[c_0_28,c_0_29]) ).
cnf(c_0_32,negated_conjecture,
( m_Ack(esk7_0,esk6_0) = m_Ack(esk10_0,esk9_0)
| index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm
| ~ epred1_3(X2,X3,X4)
| ~ setIn(X1,alive) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_31]),c_0_20])]) ).
cnf(c_0_33,negated_conjecture,
index(status,host(esk8_0)) = norm,
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_34,negated_conjecture,
index(ldr,host(esk8_0)) = host(esk8_0),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_35,negated_conjecture,
setIn(esk8_0,alive),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
fof(c_0_36,plain,
! [X226,X227,X228,X229] :
( X226 = X227
| m_Ack(X226,X228) != m_Ack(X227,X229) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_31])]) ).
cnf(c_0_37,negated_conjecture,
( m_Ack(esk7_0,esk6_0) = m_Ack(esk10_0,esk9_0)
| ~ epred1_3(X1,X2,X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_34]),c_0_35])]) ).
cnf(c_0_38,negated_conjecture,
epred1_3(esk5_0,esk7_0,esk6_0),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
fof(c_0_39,plain,
! [X255,X256,X257] :
( ( ~ elem(X255,cons(X256,X257))
| X255 = X256
| elem(X255,X257) )
& ( X255 != X256
| elem(X255,cons(X256,X257)) )
& ( ~ elem(X255,X257)
| elem(X255,cons(X256,X257)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_46])])]) ).
cnf(c_0_40,plain,
( X1 = X2
| m_Ack(X1,X3) != m_Ack(X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_41,negated_conjecture,
m_Ack(esk7_0,esk6_0) = m_Ack(esk10_0,esk9_0),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_42,plain,
( elem(X1,cons(X2,X3))
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_43,plain,
( queue(host(X1)) = cons(m_Halt(X2),X3)
| ~ epred1_3(X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_44,negated_conjecture,
( esk7_0 = X1
| m_Ack(esk10_0,esk9_0) != m_Ack(X1,X2) ),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_45,plain,
elem(X1,cons(X1,X2)),
inference(er,[status(thm)],[c_0_42]) ).
cnf(c_0_46,negated_conjecture,
cons(m_Halt(esk7_0),esk5_0) = queue(host(esk6_0)),
inference(spm,[status(thm)],[c_0_43,c_0_38]) ).
fof(c_0_47,plain,
! [X230,X231,X232,X233] :
( X232 = X233
| m_Ack(X230,X232) != m_Ack(X231,X233) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_32])]) ).
cnf(c_0_48,negated_conjecture,
esk7_0 = esk10_0,
inference(er,[status(thm)],[c_0_44]) ).
cnf(c_0_49,plain,
( leq(index(pendack,host(X1)),host(X2))
| ~ setIn(X1,alive)
| ~ elem(m_Halt(X1),queue(host(X3)))
| index(status,host(X1)) != elec_2
| ~ setIn(X2,alive)
| index(ldr,host(X2)) != host(X2)
| index(status,host(X2)) != norm
| ~ epred1_3(X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_50,negated_conjecture,
elem(m_Halt(esk7_0),queue(host(esk6_0))),
inference(spm,[status(thm)],[c_0_45,c_0_46]) ).
cnf(c_0_51,negated_conjecture,
host(esk7_0) = host(esk10_0),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_52,plain,
( X1 = X2
| m_Ack(X3,X1) != m_Ack(X4,X2) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_53,negated_conjecture,
m_Ack(esk10_0,esk9_0) = m_Ack(esk10_0,esk6_0),
inference(rw,[status(thm)],[c_0_41,c_0_48]) ).
cnf(c_0_54,negated_conjecture,
( leq(nbr_proc,host(X1))
| index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm
| ~ epred1_3(X2,X3,X4)
| ~ setIn(esk7_0,alive)
| ~ setIn(X1,alive) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_50]),c_0_51]),c_0_13]),c_0_20]),c_0_51]),c_0_25])]) ).
cnf(c_0_55,negated_conjecture,
( esk9_0 = X1
| m_Ack(esk10_0,esk6_0) != m_Ack(X2,X1) ),
inference(spm,[status(thm)],[c_0_52,c_0_53]) ).
cnf(c_0_56,negated_conjecture,
( leq(nbr_proc,host(X1))
| index(ldr,host(X1)) != host(X1)
| index(status,host(X1)) != norm
| ~ epred1_3(X2,X3,X4)
| ~ setIn(X1,alive) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_54,c_0_48]),c_0_27])]) ).
cnf(c_0_57,negated_conjecture,
esk9_0 = esk6_0,
inference(er,[status(thm)],[c_0_55]) ).
cnf(c_0_58,negated_conjecture,
( leq(nbr_proc,host(esk8_0))
| ~ epred1_3(X1,X2,X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_33]),c_0_34]),c_0_35])]) ).
cnf(c_0_59,negated_conjecture,
epred1_3(esk5_0,esk10_0,esk6_0),
inference(rw,[status(thm)],[c_0_38,c_0_48]) ).
cnf(c_0_60,negated_conjecture,
host(esk6_0) != host(esk8_0),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_61,negated_conjecture,
host(esk6_0) = nbr_proc,
inference(rw,[status(thm)],[c_0_20,c_0_57]) ).
cnf(c_0_62,negated_conjecture,
leq(nbr_proc,host(esk8_0)),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_63,negated_conjecture,
host(esk8_0) != nbr_proc,
inference(rw,[status(thm)],[c_0_60,c_0_61]) ).
cnf(c_0_64,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16,c_0_62]),c_0_18])]),c_0_63]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV457+1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n013.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 05:16:56 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 8.34/5.76 % Version : CSE_E---1.7
% 8.34/5.76 % Problem : theBenchmark.p
% 8.34/5.76 % SZS status Theorem for theBenchmark.p
% 8.34/5.76 % SZS output start CNFRefutation
% See solution above
% 8.34/5.79 % Total time : 4.369s
%------------------------------------------------------------------------------