%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV469+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.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 : Fri Sep 25 03:13:23 PM UTC 2026
% Result : Theorem 71.12s 9.55s
% Output : Proof 71.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 10
% Syntax : Number of formulae : 76 ( 30 unt; 0 def)
% Number of atoms : 599 ( 268 equ)
% Maximal formula atoms : 108 ( 7 avg)
% Number of connectives : 825 ( 302 ~; 232 |; 233 &)
% ( 4 <=>; 54 =>; 0 <=; 0 <~>)
% Maximal formula depth : 37 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 17 con; 0-3 aty)
% Number of variables : 219 ( 6 sgn 176 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f64,axiom,
! [X,Y] :
( leq(X,s(Y))
<=> ( leq(X,Y)
| X = s(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_64) ).
fof(f64_nnf,plain,
! [X,Y] :
( ( ( ~ leq(X,Y)
& X != s(Y) )
| leq(X,s(Y)) )
& ( leq(X,Y)
| X = s(Y)
| ~ leq(X,s(Y)) ) ),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
! [X,Y] :
( ( ( ~ leq(X,Y)
& X != s(Y) )
| leq(X,s(Y)) )
& ( leq(X,Y)
| X = s(Y)
| ~ leq(X,s(Y)) ) ),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c92,plain,
( leq(X0,X1)
| X0 = s(X1)
| ~ leq(X0,s(X1)) ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
fof(f60,axiom,
! [X,Y] :
( leq(Y,X)
| leq(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_60) ).
fof(f60_nnf,plain,
! [X,Y] :
( leq(Y,X)
| leq(X,Y) ),
inference(nnf_transformation,[status(thm)],[f60]) ).
fof(f60_sk,plain,
! [X,Y] :
( leq(Y,X)
| leq(X,Y) ),
inference(skolemisation,[status(esa)],[f60_nnf]) ).
cnf(c85,plain,
( leq(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
fof(f66,conjecture,
! [V,W,X,Y] :
( ( queue(host(X)) = cons(m_Down(Y),V)
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& elem(m_Down(Pid20),queue(host(Pid0)))
& ~ leq(host(Pid0),host(Z))
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& 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,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,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& 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,Pid20,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& host(Pid20) = host(Pid0)
& setIn(Pid0,alive) )
=> ~ ( elem(m_Down(Pid20),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& host(Pid0) = host(Pid20)
& elem(m_Down(Pid20),queue(host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [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,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( 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(Pid0)),host(Z)) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& host(Pid0) = host(Pid20)
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Pid0),host(Z)) )
=> ~ elem(m_Down(Pid20),queue(host(Z))) )
& ! [Z,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& setIn(Pid0,alive) )
=> ~ ( setIn(host(Pid0),index(down,host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& setIn(host(Pid0),index(down,host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [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_2
& setIn(Pid0,alive) )
=> ~ elem(m_Ack(Z,Pid0),queue(host(Z))) )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid0] :
( elem(m_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( ~ leq(host(X),host(Y))
=> ( ~ ( ( host(Y) = host(index(elid,host(X)))
& index(status,host(X)) = wait )
| ( index(status,host(X)) = norm
& index(ldr,host(X)) = host(Y) ) )
=> ( ( index(status,host(X)) = elec_1
& ! [Z] :
( ( leq(s(zero),Z)
& ~ leq(host(X),Z) )
=> ( Z = host(Y)
| setIn(Z,index(down,host(X))) ) ) )
=> ( ~ leq(nbr_proc,host(X))
=> ! [Z] :
( host(X) != host(Z)
=> ! [W0] :
( host(X) = host(W0)
=> ( ( setIn(W0,alive)
& ~ leq(s(host(X)),host(Z)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
fof(f66_neg,negated_conjecture,
~ ! [V,W,X,Y] :
( ( queue(host(X)) = cons(m_Down(Y),V)
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_1
& elem(m_Down(Pid20),queue(host(Pid0)))
& ~ leq(host(Pid0),host(Z))
& ! [V0] :
( ( leq(s(zero),V0)
& ~ leq(host(Pid0),V0) )
=> ( V0 = host(Pid20)
| setIn(V0,index(down,host(Pid0))) ) ) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& 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,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,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& 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,Pid20,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& host(Pid20) = host(Pid0)
& setIn(Pid0,alive) )
=> ~ ( elem(m_Down(Pid20),queue(host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& host(Pid0) = host(Pid20)
& elem(m_Down(Pid20),queue(host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [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,Pid20,Pid0] :
( ( host(Pid20) = host(Z)
& elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( 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(Pid0)),host(Z)) )
& ! [Z,Pid20,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& host(Pid0) = host(Pid20)
& setIn(Pid0,alive)
& setIn(Z,alive)
& ~ leq(host(Pid0),host(Z)) )
=> ~ elem(m_Down(Pid20),queue(host(Z))) )
& ! [Z,Pid0] :
( ( index(ldr,host(Pid0)) = host(Pid0)
& index(status,host(Pid0)) = norm
& setIn(Pid0,alive) )
=> ~ ( setIn(host(Pid0),index(down,host(Z)))
& setIn(Z,alive) ) )
& ! [Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& setIn(host(Pid0),index(down,host(Z)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> leq(index(pendack,host(Pid0)),host(Z)) )
& ! [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_2
& setIn(Pid0,alive) )
=> ~ elem(m_Ack(Z,Pid0),queue(host(Z))) )
& ! [Z,Pid0] :
( ( host(Pid0) = host(Z)
& Pid0 != Z )
=> ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) ) )
& ! [Z,Pid0] :
( elem(m_Ldr(Pid0),queue(host(Z)))
=> ~ leq(host(Z),host(Pid0)) ) )
=> ( setIn(X,alive)
=> ( ~ leq(host(X),host(Y))
=> ( ~ ( ( host(Y) = host(index(elid,host(X)))
& index(status,host(X)) = wait )
| ( index(status,host(X)) = norm
& index(ldr,host(X)) = host(Y) ) )
=> ( ( index(status,host(X)) = elec_1
& ! [Z] :
( ( leq(s(zero),Z)
& ~ leq(host(X),Z) )
=> ( Z = host(Y)
| setIn(Z,index(down,host(X))) ) ) )
=> ( ~ leq(nbr_proc,host(X))
=> ! [Z] :
( host(X) != host(Z)
=> ! [W0] :
( host(X) = host(W0)
=> ( ( setIn(W0,alive)
& ~ leq(s(host(X)),host(Z)) )
=> ~ ( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f66]) ).
fof(f66_nnf,plain,
? [V,W,X,Y] :
( ? [Z] :
( ? [W0] :
( index(status,host(Z)) = norm
& index(ldr,host(Z)) = host(Z)
& setIn(Z,alive)
& setIn(W0,alive)
& ~ leq(s(host(X)),host(Z))
& host(X) = host(W0) )
& host(X) != host(Z) )
& ~ leq(nbr_proc,host(X))
& index(status,host(X)) = elec_1
& ! [Z] :
( Z = host(Y)
| setIn(Z,index(down,host(X)))
| ~ leq(s(zero),Z)
| leq(host(X),Z) )
& ( host(Y) != host(index(elid,host(X)))
| index(status,host(X)) != wait )
& ( index(status,host(X)) != norm
| index(ldr,host(X)) != host(Y) )
& ~ leq(host(X),host(Y))
& setIn(X,alive)
& queue(host(X)) = cons(m_Down(Y),V)
& ! [Z,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_1
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| leq(host(Pid0),host(Z))
| ? [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
| host(Pid20) != host(Z)
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [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,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_2
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Z)) )
& ! [Z,Pid20,Pid0] :
( ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Z,alive)
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| host(Pid20) != host(Pid0)
| ~ setIn(Pid0,alive) )
& ! [Z,Pid20,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| host(Pid0) != host(Pid20)
| ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [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,Pid20,Pid0] :
( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| host(Pid20) != host(Z)
| ~ elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,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] :
( ~ elem(m_Down(Pid20),queue(host(Z)))
| index(status,host(Pid0)) != elec_2
| host(Pid0) != host(Pid20)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Pid0),host(Z)) )
& ! [Z,Pid0] :
( ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Z,alive)
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,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(Z,Pid0),queue(host(Z)))
| index(status,host(Pid0)) != elec_2
| ~ setIn(Pid0,alive) )
& ! [Z,Pid0] :
( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ! [Z,Pid0] :
( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ldr(Pid0),queue(host(Z))) ) ),
inference(nnf_transformation,[status(thm)],[f66_neg]) ).
fof(f66_sk,plain,
! [Pid0,Z,Pid20] :
( index(status,host(sk8)) = norm
& index(ldr,host(sk8)) = host(sk8)
& setIn(sk8,alive)
& setIn(sk9,alive)
& ~ leq(s(host(sk5)),host(sk8))
& host(sk5) = host(sk9)
& host(sk5) != host(sk8)
& ~ leq(nbr_proc,host(sk5))
& index(status,host(sk5)) = elec_1
& ( Z = host(sk6)
| setIn(Z,index(down,host(sk5)))
| ~ leq(s(zero),Z)
| leq(host(sk5),Z) )
& ( host(sk6) != host(index(elid,host(sk5)))
| index(status,host(sk5)) != wait )
& ( index(status,host(sk5)) != norm
| index(ldr,host(sk5)) != host(sk6) )
& ~ leq(host(sk5),host(sk6))
& setIn(sk5,alive)
& queue(host(sk5)) = cons(m_Down(sk6),sk3)
& ( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_1
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| leq(host(Pid0),host(Z))
| ( sk7(Z,Pid20,Pid0) != host(Pid20)
& ~ setIn(sk7(Z,Pid20,Pid0),index(down,host(Pid0)))
& leq(s(zero),sk7(Z,Pid20,Pid0))
& ~ leq(host(Pid0),sk7(Z,Pid20,Pid0)) ) )
& ( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_2
| host(Pid20) != host(Z)
| ~ elem(m_Down(Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ( ~ 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)) )
& ( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| index(status,host(Pid0)) != elec_2
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Z)) )
& ( ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Z,alive)
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| host(Pid20) != host(Pid0)
| ~ setIn(Pid0,alive) )
& ( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| host(Pid0) != host(Pid20)
| ~ elem(m_Down(Pid20),queue(host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ( ~ 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) )
& ( index(status,host(Z)) != norm
| index(ldr,host(Z)) != host(Z)
| ~ setIn(Z,alive)
| host(Pid20) != host(Z)
| ~ elem(m_Ack(Pid0,Pid20),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ( 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)) )
& ( ~ elem(m_Down(Pid20),queue(host(Z)))
| index(status,host(Pid0)) != elec_2
| host(Pid0) != host(Pid20)
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| leq(host(Pid0),host(Z)) )
& ( ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Z,alive)
| index(ldr,host(Pid0)) != host(Pid0)
| index(status,host(Pid0)) != norm
| ~ setIn(Pid0,alive) )
& ( leq(index(pendack,host(Pid0)),host(Z))
| index(status,host(Pid0)) != elec_2
| ~ setIn(host(Pid0),index(down,host(Z)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ( index(elid,host(Z)) = Z
| ~ setIn(Z,alive)
| ( index(status,host(Z)) != elec_2
& index(status,host(Z)) != elec_1 ) )
& ( ~ elem(m_Ack(Z,Pid0),queue(host(Z)))
| index(status,host(Pid0)) != elec_2
| ~ setIn(Pid0,alive) )
& ( ~ setIn(Pid0,alive)
| ~ setIn(Z,alive)
| host(Pid0) != host(Z)
| Pid0 = Z )
& ( ~ leq(host(Z),host(Pid0))
| ~ elem(m_Ldr(Pid0),queue(host(Z))) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4,sk5,sk6,sk7,sk8,sk9])],[f66_nnf]) ).
cnf(c126,plain,
~ leq(s(host(sk5)),host(sk8)),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p259,plain,
leq(host(sk8),s(host(sk5))),
inference(resolution,[status(thm)],[c85,c126]) ).
cnf(p1206,plain,
( leq(host(sk8),host(sk5))
| host(sk8) = s(host(sk5)) ),
inference(resolution,[status(thm)],[c92,p259]) ).
cnf(p1473,plain,
( ~ leq(host(sk8),host(sk8))
| leq(host(sk8),host(sk5)) ),
inference(superposition,[status(thm)],[p1206,c126]) ).
fof(f59,axiom,
! [X] : leq(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_59) ).
fof(f59_nnf,plain,
! [X] : leq(X,X),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [X] : leq(X,X),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c84,plain,
leq(X0,X0),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(p1504,plain,
leq(host(sk8),host(sk5)),
inference(resolution,[status(thm)],[p1473,c84]) ).
fof(f61,axiom,
! [X,Y] :
( ( leq(Y,X)
& leq(X,Y) )
<=> X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_61) ).
fof(f61_nnf,plain,
! [X,Y] :
( ( X != Y
| ( leq(Y,X)
& leq(X,Y) ) )
& ( X = Y
| ~ leq(Y,X)
| ~ leq(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [X,Y] :
( ( X != Y
| ( leq(Y,X)
& leq(X,Y) ) )
& ( X = Y
| ~ leq(Y,X)
| ~ leq(X,Y) ) ),
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c86,plain,
( X0 = X1
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(p1505,plain,
( host(sk8) = host(sk5)
| ~ leq(host(sk5),host(sk8)) ),
inference(resolution,[status(thm)],[p1504,c86]) ).
cnf(c102,plain,
( ~ setIn(host(X5),index(down,host(X4)))
| ~ setIn(X4,alive)
| index(ldr,host(X5)) != host(X5)
| index(status,host(X5)) != norm
| ~ setIn(X5,alive) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c128,plain,
setIn(sk8,alive),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p161,plain,
( ~ setIn(host(sk8),index(down,host(X0)))
| ~ setIn(X0,alive)
| host(sk8) != host(sk8)
| norm != norm ),
inference(resolution,[status(thm)],[c102,c128]) ).
cnf(p230,plain,
( ~ setIn(host(sk8),index(down,host(X0)))
| ~ setIn(X0,alive)
| norm != norm ),
inference(equality_resolution,[status(thm)],[p161]) ).
cnf(p231,plain,
( ~ setIn(host(sk8),index(down,host(X0)))
| ~ setIn(X0,alive) ),
inference(equality_resolution,[status(thm)],[p230]) ).
cnf(c117,plain,
setIn(sk5,alive),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p232,plain,
~ setIn(host(sk8),index(down,host(sk5))),
inference(resolution,[status(thm)],[p231,c117]) ).
cnf(c121,plain,
( X4 = host(sk6)
| setIn(X4,index(down,host(sk5)))
| ~ leq(s(zero),X4)
| leq(host(sk5),X4) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
fof(f2,axiom,
! [P] : leq(s(zero),host(P)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_02) ).
fof(f2_nnf,plain,
! [P] : leq(s(zero),host(P)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [P] : leq(s(zero),host(P)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c3,plain,
leq(s(zero),host(X0)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p147,plain,
( host(X0) = host(sk6)
| setIn(host(X0),index(down,host(sk5)))
| leq(host(sk5),host(X0)) ),
inference(resolution,[status(thm)],[c121,c3]) ).
cnf(p234,plain,
( host(sk8) = host(sk6)
| leq(host(sk5),host(sk8)) ),
inference(resolution,[status(thm)],[p232,p147]) ).
cnf(p1563,plain,
( host(sk8) = host(sk6)
| host(sk8) = host(sk5) ),
inference(resolution,[status(thm)],[p1505,p234]) ).
fof(f26,axiom,
! [X,Y] :
( X != Y
<=> m_Halt(X) != m_Halt(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_26) ).
fof(f26_nnf,plain,
! [X,Y] :
( ( m_Halt(X) = m_Halt(Y)
| X != Y )
& ( m_Halt(X) != m_Halt(Y)
| X = Y ) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X,Y] :
( ( m_Halt(X) = m_Halt(Y)
| X != Y )
& ( m_Halt(X) != m_Halt(Y)
| X = Y ) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c28,plain,
( m_Halt(X0) = m_Halt(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p1623,plain,
( m_Halt(host(sk8)) = m_Halt(host(sk6))
| host(sk8) = host(sk5) ),
inference(resolution,[status(thm)],[p1563,c28]) ).
fof(f49,axiom,
! [X] : pidMsg(m_Halt(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_49) ).
fof(f49_nnf,plain,
! [X] : pidMsg(m_Halt(X)) = X,
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [X] : pidMsg(m_Halt(X)) = X,
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c61,plain,
pidMsg(m_Halt(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p2963,plain,
( host(sk6) = host(sk8)
| host(sk8) = host(sk5) ),
inference(superposition,[status(thm)],[p1623,c61]) ).
cnf(c130,plain,
index(status,host(sk8)) = norm,
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p2979,plain,
( elec_1 = norm
| host(sk6) = host(sk8) ),
inference(superposition,[status(thm)],[p2963,c130]) ).
cnf(c108,plain,
( ~ elem(m_Down(X6),queue(host(X4)))
| ~ setIn(X4,alive)
| index(ldr,host(X5)) != host(X5)
| index(status,host(X5)) != norm
| host(X6) != host(X5)
| ~ setIn(X5,alive) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p178,plain,
( ~ elem(m_Down(X0),queue(host(X1)))
| ~ setIn(X1,alive)
| host(sk8) != host(sk8)
| norm != norm
| host(X0) != host(sk8) ),
inference(resolution,[status(thm)],[c108,c128]) ).
cnf(p205,plain,
( ~ elem(m_Down(X0),queue(host(X1)))
| ~ setIn(X1,alive)
| norm != norm
| host(X0) != host(sk8) ),
inference(equality_resolution,[status(thm)],[p178]) ).
cnf(p207,plain,
( ~ elem(m_Down(X0),queue(host(X1)))
| ~ setIn(X1,alive)
| host(X0) != host(sk8) ),
inference(equality_resolution,[status(thm)],[p205]) ).
cnf(p3092,plain,
( ~ elem(m_Down(sk6),queue(host(X0)))
| ~ setIn(X0,alive)
| elec_1 = norm ),
inference(resolution,[status(thm)],[p2979,p207]) ).
cnf(p6958,plain,
( ~ elem(m_Down(sk6),queue(host(sk5)))
| elec_1 = norm ),
inference(resolution,[status(thm)],[p3092,c117]) ).
cnf(c116,plain,
queue(host(sk5)) = cons(m_Down(sk6),sk3),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p235,plain,
m_Halt(queue(host(sk5))) = m_Halt(cons(m_Down(sk6),sk3)),
inference(resolution,[status(thm)],[c28,c116]) ).
cnf(c27,plain,
( m_Halt(X0) != m_Halt(X1)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p236,plain,
( m_Halt(queue(host(sk5))) != m_Halt(X0)
| cons(m_Down(sk6),sk3) = X0 ),
inference(superposition,[status(thm)],[p235,c27]) ).
cnf(p242,plain,
cons(m_Down(sk6),sk3) = queue(host(sk5)),
inference(equality_resolution,[status(thm)],[p236]) ).
fof(f46,axiom,
! [X,Y,Q] :
( elem(X,cons(Y,Q))
<=> ( elem(X,Q)
| X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_46) ).
fof(f46_nnf,plain,
! [X,Y,Q] :
( ( ( ~ elem(X,Q)
& X != Y )
| elem(X,cons(Y,Q)) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,cons(Y,Q)) ) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
! [X,Y,Q] :
( ( ( ~ elem(X,Q)
& X != Y )
| elem(X,cons(Y,Q)) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,cons(Y,Q)) ) ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c53,plain,
( X0 != X1
| elem(X0,cons(X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p335,plain,
elem(X0,cons(X0,X1)),
inference(equality_resolution,[status(thm)],[c53]) ).
cnf(p2510,plain,
elem(m_Down(sk6),queue(host(sk5))),
inference(superposition,[status(thm)],[p242,p335]) ).
cnf(p6959,plain,
elec_1 = norm,
inference(resolution,[status(thm)],[p6958,p2510]) ).
fof(f7,axiom,
elec_1 != norm,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_07) ).
fof(f7_nnf,plain,
elec_1 != norm,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
elec_1 != norm,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c8,plain,
elec_1 != norm,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p6960,plain,
$false,
inference(resolution,[status(thm)],[p6959,c8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV469+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n001.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 19:55:38 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 71.12/9.55 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 71.12/9.55 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------