%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV457+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 : n008.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:22 PM UTC 2026
% Result : Theorem 169.43s 21.92s
% Output : Proof 169.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 44
% Syntax : Number of formulae : 335 ( 296 unt; 0 def)
% Number of atoms : 703 ( 430 equ)
% Maximal formula atoms : 72 ( 2 avg)
% Number of connectives : 707 ( 339 ~; 155 |; 165 &)
% ( 3 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 34 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 23 con; 0-4 aty)
% Number of variables : 545 ( 86 sgn 306 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f66,conjecture,
! [V,W,X] :
( ( queue(host(W)) = cons(m_Halt(X),V)
& ! [Y,Z,Pid0] :
( ( host(Z) = index(pendack,host(Pid0))
& index(status,host(Pid0)) = elec_2
& leq(nbr_proc,index(pendack,host(Pid0)))
& elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Y)) = norm
& index(ldr,host(Y)) = host(Y)
& setIn(Y,alive) ) )
& ! [Y,Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& elem(m_Halt(Pid0),queue(host(Z)))
& setIn(Pid0,alive)
& ~ leq(index(pendack,host(Pid0)),host(Y)) )
=> ~ ( index(status,host(Y)) = norm
& index(ldr,host(Y)) = host(Y)
& setIn(Y,alive) ) )
& ! [Y,Z] :
( ( index(status,host(Z)) = elec_2
& index(status,host(Y)) = elec_2
& setIn(Z,alive)
& setIn(Y,alive)
& ~ leq(host(Y),host(Z)) )
=> ~ leq(index(pendack,host(Y)),index(pendack,host(Z))) )
& ! [Y,Z,Pid0] :
( ( host(Z) = host(Y)
& elem(m_Ack(Pid0,Y),queue(host(Pid0)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> ~ setIn(host(Pid0),index(down,host(Z))) )
& ! [Y,Z,Pid0] :
( ( host(Pid0) = host(Y)
& elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& elem(m_Down(Y),queue(host(Z))) )
=> ~ setIn(Pid0,alive) )
& ! [Y] :
( ( setIn(Y,alive)
& ( index(status,host(Y)) = elec_2
| index(status,host(Y)) = elec_1 ) )
=> index(elid,host(Y)) = Y )
& ! [Y,Z] :
( ( index(status,host(Z)) = elec_1
& setIn(Z,alive) )
=> ~ elem(m_Ack(Z,Y),queue(host(Z))) )
& ! [Y,Z] :
( ( index(status,host(Z)) = elec_1
& setIn(Z,alive) )
=> ~ elem(m_Ack(Y,Z),queue(host(Y))) )
& ! [Y,Z] :
( ( elem(m_Ack(Z,Y),queue(host(Z)))
& setIn(Z,alive) )
=> leq(host(Y),index(pendack,host(Z))) )
& ! [Y,Z] :
( ( host(Z) = host(Y)
& Z != Y )
=> ( ~ setIn(Z,alive)
| ~ setIn(Y,alive) ) )
& ! [Y,Z] :
( ( host(Z) = host(Y)
& leq(Z,Y)
& ~ setIn(Y,alive) )
=> ~ setIn(Z,alive) )
& ! [Y,Z,Pid0] :
( elem(m_Ack(Pid0,Y),queue(host(Z)))
=> ~ leq(host(Y),host(Pid0)) )
& ! [Y,Z] :
( elem(m_Ldr(Z),queue(host(Y)))
=> ~ leq(host(Y),host(Z)) )
& ! [Y,Z] :
( elem(m_Down(Z),queue(host(Y)))
=> ~ setIn(Z,alive) )
& ! [Y,Z] :
( elem(m_Ack(Z,Y),queue(host(Z)))
=> setIn(Z,pids) ) )
=> ( setIn(W,alive)
=> ! [Y] :
( host(W) != host(Y)
=> ! [Z,X0] :
( host(X) = host(X0)
=> ( host(W) != host(X0)
=> ( ( host(Z) = index(pendack,host(X0))
& index(status,host(X0)) = elec_2
& elem(m_Ack(X0,Z),snoc(queue(host(X0)),m_Ack(X,W)))
& leq(nbr_proc,index(pendack,host(X0)))
& setIn(X0,alive) )
=> ~ ( index(status,host(Y)) = norm
& index(ldr,host(Y)) = host(Y)
& setIn(Y,alive) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
fof(f66_neg,negated_conjecture,
~ ! [V,W,X] :
( ( queue(host(W)) = cons(m_Halt(X),V)
& ! [Y,Z,Pid0] :
( ( host(Z) = index(pendack,host(Pid0))
& index(status,host(Pid0)) = elec_2
& leq(nbr_proc,index(pendack,host(Pid0)))
& elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& setIn(Pid0,alive) )
=> ~ ( index(status,host(Y)) = norm
& index(ldr,host(Y)) = host(Y)
& setIn(Y,alive) ) )
& ! [Y,Z,Pid0] :
( ( index(status,host(Pid0)) = elec_2
& elem(m_Halt(Pid0),queue(host(Z)))
& setIn(Pid0,alive)
& ~ leq(index(pendack,host(Pid0)),host(Y)) )
=> ~ ( index(status,host(Y)) = norm
& index(ldr,host(Y)) = host(Y)
& setIn(Y,alive) ) )
& ! [Y,Z] :
( ( index(status,host(Z)) = elec_2
& index(status,host(Y)) = elec_2
& setIn(Z,alive)
& setIn(Y,alive)
& ~ leq(host(Y),host(Z)) )
=> ~ leq(index(pendack,host(Y)),index(pendack,host(Z))) )
& ! [Y,Z,Pid0] :
( ( host(Z) = host(Y)
& elem(m_Ack(Pid0,Y),queue(host(Pid0)))
& setIn(Pid0,alive)
& setIn(Z,alive) )
=> ~ setIn(host(Pid0),index(down,host(Z))) )
& ! [Y,Z,Pid0] :
( ( host(Pid0) = host(Y)
& elem(m_Ack(Pid0,Z),queue(host(Pid0)))
& elem(m_Down(Y),queue(host(Z))) )
=> ~ setIn(Pid0,alive) )
& ! [Y] :
( ( setIn(Y,alive)
& ( index(status,host(Y)) = elec_2
| index(status,host(Y)) = elec_1 ) )
=> index(elid,host(Y)) = Y )
& ! [Y,Z] :
( ( index(status,host(Z)) = elec_1
& setIn(Z,alive) )
=> ~ elem(m_Ack(Z,Y),queue(host(Z))) )
& ! [Y,Z] :
( ( index(status,host(Z)) = elec_1
& setIn(Z,alive) )
=> ~ elem(m_Ack(Y,Z),queue(host(Y))) )
& ! [Y,Z] :
( ( elem(m_Ack(Z,Y),queue(host(Z)))
& setIn(Z,alive) )
=> leq(host(Y),index(pendack,host(Z))) )
& ! [Y,Z] :
( ( host(Z) = host(Y)
& Z != Y )
=> ( ~ setIn(Z,alive)
| ~ setIn(Y,alive) ) )
& ! [Y,Z] :
( ( host(Z) = host(Y)
& leq(Z,Y)
& ~ setIn(Y,alive) )
=> ~ setIn(Z,alive) )
& ! [Y,Z,Pid0] :
( elem(m_Ack(Pid0,Y),queue(host(Z)))
=> ~ leq(host(Y),host(Pid0)) )
& ! [Y,Z] :
( elem(m_Ldr(Z),queue(host(Y)))
=> ~ leq(host(Y),host(Z)) )
& ! [Y,Z] :
( elem(m_Down(Z),queue(host(Y)))
=> ~ setIn(Z,alive) )
& ! [Y,Z] :
( elem(m_Ack(Z,Y),queue(host(Z)))
=> setIn(Z,pids) ) )
=> ( setIn(W,alive)
=> ! [Y] :
( host(W) != host(Y)
=> ! [Z,X0] :
( host(X) = host(X0)
=> ( host(W) != host(X0)
=> ( ( host(Z) = index(pendack,host(X0))
& index(status,host(X0)) = elec_2
& elem(m_Ack(X0,Z),snoc(queue(host(X0)),m_Ack(X,W)))
& leq(nbr_proc,index(pendack,host(X0)))
& setIn(X0,alive) )
=> ~ ( index(status,host(Y)) = norm
& index(ldr,host(Y)) = host(Y)
& setIn(Y,alive) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f66]) ).
fof(f66_nnf,plain,
? [V,W,X] :
( ? [Y] :
( ? [Z,X0] :
( index(status,host(Y)) = norm
& index(ldr,host(Y)) = host(Y)
& setIn(Y,alive)
& host(Z) = index(pendack,host(X0))
& index(status,host(X0)) = elec_2
& elem(m_Ack(X0,Z),snoc(queue(host(X0)),m_Ack(X,W)))
& leq(nbr_proc,index(pendack,host(X0)))
& setIn(X0,alive)
& host(W) != host(X0)
& host(X) = host(X0) )
& host(W) != host(Y) )
& setIn(W,alive)
& queue(host(W)) = cons(m_Halt(X),V)
& ! [Y,Z,Pid0] :
( index(status,host(Y)) != norm
| index(ldr,host(Y)) != host(Y)
| ~ setIn(Y,alive)
| host(Z) != index(pendack,host(Pid0))
| index(status,host(Pid0)) != elec_2
| ~ leq(nbr_proc,index(pendack,host(Pid0)))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ! [Y,Z,Pid0] :
( index(status,host(Y)) != norm
| index(ldr,host(Y)) != host(Y)
| ~ setIn(Y,alive)
| index(status,host(Pid0)) != elec_2
| ~ elem(m_Halt(Pid0),queue(host(Z)))
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Y)) )
& ! [Y,Z] :
( ~ leq(index(pendack,host(Y)),index(pendack,host(Z)))
| index(status,host(Z)) != elec_2
| index(status,host(Y)) != elec_2
| ~ setIn(Z,alive)
| ~ setIn(Y,alive)
| leq(host(Y),host(Z)) )
& ! [Y,Z,Pid0] :
( ~ setIn(host(Pid0),index(down,host(Z)))
| host(Z) != host(Y)
| ~ elem(m_Ack(Pid0,Y),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ! [Y,Z,Pid0] :
( ~ setIn(Pid0,alive)
| host(Pid0) != host(Y)
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ elem(m_Down(Y),queue(host(Z))) )
& ! [Y] :
( index(elid,host(Y)) = Y
| ~ setIn(Y,alive)
| ( index(status,host(Y)) != elec_2
& index(status,host(Y)) != elec_1 ) )
& ! [Y,Z] :
( ~ elem(m_Ack(Z,Y),queue(host(Z)))
| index(status,host(Z)) != elec_1
| ~ setIn(Z,alive) )
& ! [Y,Z] :
( ~ elem(m_Ack(Y,Z),queue(host(Y)))
| index(status,host(Z)) != elec_1
| ~ setIn(Z,alive) )
& ! [Y,Z] :
( leq(host(Y),index(pendack,host(Z)))
| ~ elem(m_Ack(Z,Y),queue(host(Z)))
| ~ setIn(Z,alive) )
& ! [Y,Z] :
( ~ setIn(Z,alive)
| ~ setIn(Y,alive)
| host(Z) != host(Y)
| Z = Y )
& ! [Y,Z] :
( ~ setIn(Z,alive)
| host(Z) != host(Y)
| ~ leq(Z,Y)
| setIn(Y,alive) )
& ! [Y,Z,Pid0] :
( ~ leq(host(Y),host(Pid0))
| ~ elem(m_Ack(Pid0,Y),queue(host(Z))) )
& ! [Y,Z] :
( ~ leq(host(Y),host(Z))
| ~ elem(m_Ldr(Z),queue(host(Y))) )
& ! [Y,Z] :
( ~ setIn(Z,alive)
| ~ elem(m_Down(Z),queue(host(Y))) )
& ! [Y,Z] :
( setIn(Z,pids)
| ~ elem(m_Ack(Z,Y),queue(host(Z))) ) ),
inference(nnf_transformation,[status(thm)],[f66_neg]) ).
fof(f66_sk,plain,
! [Z,Y,Pid0] :
( index(status,host(sk6)) = norm
& index(ldr,host(sk6)) = host(sk6)
& setIn(sk6,alive)
& host(sk7) = index(pendack,host(sk8))
& index(status,host(sk8)) = elec_2
& elem(m_Ack(sk8,sk7),snoc(queue(host(sk8)),m_Ack(sk5,sk4)))
& leq(nbr_proc,index(pendack,host(sk8)))
& setIn(sk8,alive)
& host(sk4) != host(sk8)
& host(sk5) = host(sk8)
& host(sk4) != host(sk6)
& setIn(sk4,alive)
& queue(host(sk4)) = cons(m_Halt(sk5),sk3)
& ( index(status,host(Y)) != norm
| index(ldr,host(Y)) != host(Y)
| ~ setIn(Y,alive)
| host(Z) != index(pendack,host(Pid0))
| index(status,host(Pid0)) != elec_2
| ~ leq(nbr_proc,index(pendack,host(Pid0)))
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ setIn(Pid0,alive) )
& ( index(status,host(Y)) != norm
| index(ldr,host(Y)) != host(Y)
| ~ setIn(Y,alive)
| index(status,host(Pid0)) != elec_2
| ~ elem(m_Halt(Pid0),queue(host(Z)))
| ~ setIn(Pid0,alive)
| leq(index(pendack,host(Pid0)),host(Y)) )
& ( ~ leq(index(pendack,host(Y)),index(pendack,host(Z)))
| index(status,host(Z)) != elec_2
| index(status,host(Y)) != elec_2
| ~ setIn(Z,alive)
| ~ setIn(Y,alive)
| leq(host(Y),host(Z)) )
& ( ~ setIn(host(Pid0),index(down,host(Z)))
| host(Z) != host(Y)
| ~ elem(m_Ack(Pid0,Y),queue(host(Pid0)))
| ~ setIn(Pid0,alive)
| ~ setIn(Z,alive) )
& ( ~ setIn(Pid0,alive)
| host(Pid0) != host(Y)
| ~ elem(m_Ack(Pid0,Z),queue(host(Pid0)))
| ~ elem(m_Down(Y),queue(host(Z))) )
& ( index(elid,host(Y)) = Y
| ~ setIn(Y,alive)
| ( index(status,host(Y)) != elec_2
& index(status,host(Y)) != elec_1 ) )
& ( ~ elem(m_Ack(Z,Y),queue(host(Z)))
| index(status,host(Z)) != elec_1
| ~ setIn(Z,alive) )
& ( ~ elem(m_Ack(Y,Z),queue(host(Y)))
| index(status,host(Z)) != elec_1
| ~ setIn(Z,alive) )
& ( leq(host(Y),index(pendack,host(Z)))
| ~ elem(m_Ack(Z,Y),queue(host(Z)))
| ~ setIn(Z,alive) )
& ( ~ setIn(Z,alive)
| ~ setIn(Y,alive)
| host(Z) != host(Y)
| Z = Y )
& ( ~ setIn(Z,alive)
| host(Z) != host(Y)
| ~ leq(Z,Y)
| setIn(Y,alive) )
& ( ~ leq(host(Y),host(Pid0))
| ~ elem(m_Ack(Pid0,Y),queue(host(Z))) )
& ( ~ leq(host(Y),host(Z))
| ~ elem(m_Ldr(Z),queue(host(Y))) )
& ( ~ setIn(Z,alive)
| ~ elem(m_Down(Z),queue(host(Y))) )
& ( setIn(Z,pids)
| ~ elem(m_Ack(Z,Y),queue(host(Z))) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4,sk5,sk6,sk7,sk8])],[f66_nnf]) ).
cnf(c114,plain,
host(sk4) != host(sk6),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t147,plain,
ifeq(host(sk4),host(sk6),false,true) = true,
inference(equality_encoding,[status(esa)],[c114]) ).
cnf(t291,plain,
ifeq(host(sk4),host(sk6),false,true) = true,
inference(orient,[status(thm)],[t147]) ).
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(t215,plain,
ifeq(leq(X1,X2),true,ifeq(leq(X2,X1),true,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c86]) ).
cnf(t260,plain,
ifeq(leq(X1,X2),true,ifeq(leq(X2,X1),true,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t215]) ).
cnf(c110,plain,
( index(status,host(X3)) != norm
| index(ldr,host(X3)) != host(X3)
| ~ setIn(X3,alive)
| index(status,host(X5)) != elec_2
| ~ elem(m_Halt(X5),queue(host(X4)))
| ~ setIn(X5,alive)
| leq(index(pendack,host(X5)),host(X3)) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t253,plain,
ifeq(setIn(X1,alive),true,ifeq(elem(m_Halt(X1),queue(host(X2))),true,ifeq(index(status,host(X1)),elec_2,ifeq(setIn(X3,alive),true,ifeq(index(ldr,host(X3)),host(X3),ifeq(index(status,host(X3)),norm,leq(index(pendack,host(X1)),host(X3)),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c110]) ).
cnf(t313,plain,
ifeq(setIn(X1,alive),true,ifeq(elem(m_Halt(X1),queue(host(X2))),true,ifeq(index(status,host(X1)),elec_2,ifeq(setIn(X3,alive),true,ifeq(index(ldr,host(X3)),host(X3),ifeq(index(status,host(X3)),norm,leq(index(pendack,host(X1)),host(X3)),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t253]) ).
cnf(c88,plain,
( X0 != X1
| leq(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(hi61,axiom,
ifeq(X0,X1,leq(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c88]) ).
fof(f50,axiom,
! [X] : pidMsg(m_Down(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_50) ).
fof(f50_nnf,plain,
! [X] : pidMsg(m_Down(X)) = X,
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [X] : pidMsg(m_Down(X)) = X,
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c62,plain,
pidMsg(m_Down(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(hi36,axiom,
pidMsg(m_Down(X0)) = X0,
inference(equality_encoding,[status(esa)],[c62]) ).
cnf(h212,plain,
leq(V0,pidMsg(m_Down(V0))) = true,
inference(hyper_resolution,[status(thm)],[hi61,hi36]) ).
cnf(c100,plain,
( ~ setIn(X4,alive)
| host(X4) != host(X3)
| ~ leq(X4,X3)
| setIn(X3,alive) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(hi69,negated_conjecture,
ifeq(leq(X0,X1),true,ifeq(host(X0),host(X1),ifeq(setIn(X0,alive),true,setIn(X1,alive),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c100]) ).
cnf(c117,plain,
setIn(sk8,alive),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(hi79,negated_conjecture,
setIn(sk8,alive) = true,
inference(equality_encoding,[status(esa)],[c117]) ).
cnf(t115,plain,
setIn(pidMsg(m_Down(sk8)),alive) = true,
inference(hyper_resolution,[status(thm)],[hi69,h212,hi36,hi79]) ).
cnf(t24,plain,
pidMsg(m_Down(X1)) = X1,
inference(equality_encoding,[status(esa)],[c62]) ).
cnf(t272,plain,
pidMsg(m_Down(X1)) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t15388,plain,
setIn(sk8,alive) = true,
inference(step,[status(thm)],[t115,t272]) ).
cnf(t585,plain,
setIn(sk8,alive) = true,
inference(orient,[status(thm)],[t15388]) ).
cnf(t607,plain,
true = ifeq(true,true,ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(index(status,host(sk8)),elec_2,ifeq(setIn(X2,alive),true,ifeq(index(ldr,host(X2)),host(X2),ifeq(index(status,host(X2)),norm,leq(index(pendack,host(sk8)),host(X2)),true),true),true),true),true),true),
inference(cp,[status(thm)],[t313,t585]) ).
cnf(t78,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t78]) ).
cnf(t16812,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(index(status,host(sk8)),elec_2,ifeq(setIn(X2,alive),true,ifeq(index(ldr,host(X2)),host(X2),ifeq(index(status,host(X2)),norm,leq(index(pendack,host(sk8)),host(X2)),true),true),true),true),true),
inference(step,[status(thm)],[t607,t256]) ).
cnf(c120,plain,
index(status,host(sk8)) = elec_2,
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t36,plain,
index(status,host(sk8)) = elec_2,
inference(equality_encoding,[status(esa)],[c120]) ).
cnf(t1208,plain,
index(status,host(sk8)) = elec_2,
inference(orient,[status(thm)],[t36]) ).
cnf(t16813,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(elec_2,elec_2,ifeq(setIn(X2,alive),true,ifeq(index(ldr,host(X2)),host(X2),ifeq(index(status,host(X2)),norm,leq(index(pendack,host(sk8)),host(X2)),true),true),true),true),true),
inference(step,[status(thm)],[t16812,t1208]) ).
cnf(t16814,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(setIn(X2,alive),true,ifeq(index(ldr,host(X2)),host(X2),ifeq(index(status,host(X2)),norm,leq(index(pendack,host(sk8)),host(X2)),true),true),true),true),
inference(step,[status(thm)],[t16813,t256]) ).
cnf(c121,plain,
host(sk7) = index(pendack,host(sk8)),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t86,plain,
index(pendack,host(sk8)) = host(sk7),
inference(equality_encoding,[status(esa)],[c121]) ).
cnf(t1014,plain,
index(pendack,host(sk8)) = host(sk7),
inference(orient,[status(thm)],[t86]) ).
cnf(c118,plain,
leq(nbr_proc,index(pendack,host(sk8))),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t133,plain,
leq(nbr_proc,index(pendack,host(sk8))) = true,
inference(equality_encoding,[status(esa)],[c118]) ).
cnf(t485,plain,
leq(nbr_proc,index(pendack,host(sk8))) = true,
inference(orient,[status(thm)],[t133]) ).
cnf(t15391,plain,
leq(nbr_proc,host(sk7)) = true,
inference(step,[status(thm)],[t485,t1014]) ).
cnf(t1023,plain,
leq(nbr_proc,host(sk7)) = true,
inference(rw,[status(thm)],[t15391]) ).
cnf(t1290,plain,
leq(nbr_proc,host(sk7)) = true,
inference(orient,[status(thm)],[t1023]) ).
cnf(t1293,plain,
host(sk7) = ifeq(true,true,ifeq(leq(host(sk7),nbr_proc),true,nbr_proc,host(sk7)),host(sk7)),
inference(cp,[status(thm)],[t260,t1290]) ).
cnf(t15400,plain,
host(sk7) = ifeq(leq(host(sk7),nbr_proc),true,nbr_proc,host(sk7)),
inference(step,[status(thm)],[t1293,t256]) ).
fof(f4,axiom,
! [P] : leq(host(P),nbr_proc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_04) ).
fof(f4_nnf,plain,
! [P] : leq(host(P),nbr_proc),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [P] : leq(host(P),nbr_proc),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c5,plain,
leq(host(X0),nbr_proc),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t40,plain,
leq(host(X1),nbr_proc) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t443,plain,
leq(host(X1),nbr_proc) = true,
inference(orient,[status(thm)],[t40]) ).
cnf(t15401,plain,
host(sk7) = ifeq(true,true,nbr_proc,host(sk7)),
inference(step,[status(thm)],[t15400,t443]) ).
cnf(t15402,plain,
host(sk7) = nbr_proc,
inference(step,[status(thm)],[t15401,t256]) ).
cnf(t1304,plain,
host(sk7) = nbr_proc,
inference(orient,[status(thm)],[t15402]) ).
cnf(t15403,plain,
index(pendack,host(sk8)) = nbr_proc,
inference(step,[status(thm)],[t1014,t1304]) ).
cnf(t1305,plain,
index(pendack,host(sk8)) = nbr_proc,
inference(orient,[status(thm)],[t15403]) ).
cnf(t16815,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(setIn(X2,alive),true,ifeq(index(ldr,host(X2)),host(X2),ifeq(index(status,host(X2)),norm,leq(nbr_proc,host(X2)),true),true),true),true),
inference(step,[status(thm)],[t16814,t1305]) ).
cnf(t13375,plain,
ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(setIn(X2,alive),true,ifeq(index(ldr,host(X2)),host(X2),ifeq(index(status,host(X2)),norm,leq(nbr_proc,host(X2)),true),true),true),true) = true,
inference(orient,[status(thm)],[t16815]) ).
cnf(c122,plain,
setIn(sk6,alive),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(hi84,negated_conjecture,
setIn(sk6,alive) = true,
inference(equality_encoding,[status(esa)],[c122]) ).
cnf(t114,plain,
setIn(pidMsg(m_Down(sk6)),alive) = true,
inference(hyper_resolution,[status(thm)],[hi69,h212,hi36,hi84]) ).
cnf(t15390,plain,
setIn(sk6,alive) = true,
inference(step,[status(thm)],[t114,t272]) ).
cnf(t641,plain,
setIn(sk6,alive) = true,
inference(orient,[status(thm)],[t15390]) ).
cnf(t13378,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(true,true,ifeq(index(ldr,host(sk6)),host(sk6),ifeq(index(status,host(sk6)),norm,leq(nbr_proc,host(sk6)),true),true),true),true),
inference(cp,[status(thm)],[t13375,t641]) ).
cnf(t16816,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(index(ldr,host(sk6)),host(sk6),ifeq(index(status,host(sk6)),norm,leq(nbr_proc,host(sk6)),true),true),true),
inference(step,[status(thm)],[t13378,t256]) ).
cnf(c123,plain,
index(ldr,host(sk6)) = host(sk6),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t85,plain,
index(ldr,host(sk6)) = host(sk6),
inference(equality_encoding,[status(esa)],[c123]) ).
cnf(t1010,plain,
index(ldr,host(sk6)) = host(sk6),
inference(orient,[status(thm)],[t85]) ).
cnf(t16817,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(host(sk6),host(sk6),ifeq(index(status,host(sk6)),norm,leq(nbr_proc,host(sk6)),true),true),true),
inference(step,[status(thm)],[t16816,t1010]) ).
cnf(t16818,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(index(status,host(sk6)),norm,leq(nbr_proc,host(sk6)),true),true),
inference(step,[status(thm)],[t16817,t256]) ).
cnf(c124,plain,
index(status,host(sk6)) = norm,
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t35,plain,
index(status,host(sk6)) = norm,
inference(equality_encoding,[status(esa)],[c124]) ).
cnf(t1223,plain,
index(status,host(sk6)) = norm,
inference(orient,[status(thm)],[t35]) ).
cnf(t16819,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,ifeq(norm,norm,leq(nbr_proc,host(sk6)),true),true),
inference(step,[status(thm)],[t16818,t1223]) ).
cnf(t16820,plain,
true = ifeq(elem(m_Halt(sk8),queue(host(X1))),true,leq(nbr_proc,host(sk6)),true),
inference(step,[status(thm)],[t16819,t256]) ).
cnf(t13388,plain,
ifeq(elem(m_Halt(sk8),queue(host(X1))),true,leq(nbr_proc,host(sk6)),true) = true,
inference(orient,[status(thm)],[t16820]) ).
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(t190,plain,
ifeq(X1,X2,elem(X1,cons(X2,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t284,plain,
ifeq(X1,X2,elem(X1,cons(X2,X3)),true) = true,
inference(orient,[status(thm)],[t190]) ).
cnf(t285,plain,
true = elem(X1,cons(X1,X2)),
inference(cp,[status(thm)],[t284,t256]) ).
cnf(t1414,plain,
elem(X1,cons(X1,X2)) = true,
inference(orient,[status(thm)],[t285]) ).
cnf(c112,plain,
queue(host(sk4)) = cons(m_Halt(sk5),sk3),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t120,plain,
cons(m_Halt(sk5),sk3) = queue(host(sk4)),
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(t1240,plain,
cons(m_Halt(sk5),sk3) = queue(host(sk4)),
inference(orient,[status(thm)],[t120]) ).
cnf(t1416,plain,
true = elem(m_Halt(sk5),queue(host(sk4))),
inference(cp,[status(thm)],[t1414,t1240]) ).
cnf(t1605,plain,
elem(m_Halt(sk5),queue(host(sk4))) = true,
inference(orient,[status(thm)],[t1416]) ).
fof(f31,axiom,
! [X1,X2,Y1,Y2] :
( X1 != X2
=> m_Ack(X1,Y1) != m_Ack(X2,Y2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_31) ).
fof(f31_nnf,plain,
! [X1,X2,Y1,Y2] :
( m_Ack(X1,Y1) != m_Ack(X2,Y2)
| X1 = X2 ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [X1,X2,Y1,Y2] :
( m_Ack(X1,Y1) != m_Ack(X2,Y2)
| X1 = X2 ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c37,plain,
( m_Ack(X0,X2) != m_Ack(X1,X3)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t193,plain,
ifeq(m_Ack(X1,X2),m_Ack(X3,X4),X1,X3) = X3,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(t265,plain,
ifeq(m_Ack(X1,X2),m_Ack(X3,X4),X1,X3) = X3,
inference(orient,[status(thm)],[t193]) ).
cnf(t146,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t259,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t146]) ).
fof(f47,axiom,
! [X,Y,Q] :
( elem(X,snoc(Q,Y))
<=> ( elem(X,Q)
| X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_47) ).
fof(f47_nnf,plain,
! [X,Y,Q] :
( ( ( ~ elem(X,Q)
& X != Y )
| elem(X,snoc(Q,Y)) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,snoc(Q,Y)) ) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [X,Q,Y] :
( ( ( ~ elem(X,Q)
& X != Y )
| elem(X,snoc(Q,Y)) )
& ( elem(X,Q)
| X = Y
| ~ elem(X,snoc(Q,Y)) ) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c55,plain,
( elem(X0,X2)
| X0 = X1
| ~ elem(X0,snoc(X2,X1)) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(t222,plain,
ifeq(elem(X1,snoc(X2,X3)),true,or(eq(X1,X3),elem(X1,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c55]) ).
cnf(t303,plain,
ifeq(elem(X1,snoc(X2,X3)),true,or(eq(X1,X3),elem(X1,X2)),true) = true,
inference(orient,[status(thm)],[t222]) ).
cnf(c119,plain,
elem(m_Ack(sk8,sk7),snoc(queue(host(sk8)),m_Ack(sk5,sk4))),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t201,plain,
elem(m_Ack(sk8,sk7),snoc(queue(host(sk8)),m_Ack(sk5,sk4))) = true,
inference(equality_encoding,[status(esa)],[c119]) ).
cnf(t575,plain,
elem(m_Ack(sk8,sk7),snoc(queue(host(sk8)),m_Ack(sk5,sk4))) = true,
inference(orient,[status(thm)],[t201]) ).
cnf(t577,plain,
true = ifeq(true,true,or(eq(m_Ack(sk8,sk7),m_Ack(sk5,sk4)),elem(m_Ack(sk8,sk7),queue(host(sk8)))),true),
inference(cp,[status(thm)],[t303,t575]) ).
cnf(t15933,plain,
true = or(eq(m_Ack(sk8,sk7),m_Ack(sk5,sk4)),elem(m_Ack(sk8,sk7),queue(host(sk8)))),
inference(step,[status(thm)],[t577,t256]) ).
cnf(t5202,plain,
or(eq(m_Ack(sk8,sk7),m_Ack(sk5,sk4)),elem(m_Ack(sk8,sk7),queue(host(sk8)))) = true,
inference(orient,[status(thm)],[t15933]) ).
cnf(t130,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t851,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t130]) ).
cnf(c111,plain,
( index(status,host(X3)) != norm
| index(ldr,host(X3)) != host(X3)
| ~ setIn(X3,alive)
| host(X4) != index(pendack,host(X5))
| index(status,host(X5)) != elec_2
| ~ leq(nbr_proc,index(pendack,host(X5)))
| ~ elem(m_Ack(X5,X4),queue(host(X5)))
| ~ setIn(X5,alive) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(t254,plain,
or(not(setIn(X1,alive)),or(not(elem(m_Ack(X1,X2),queue(host(X1)))),or(not(leq(nbr_proc,index(pendack,host(X1)))),or(not(eq(index(status,host(X1)),elec_2)),or(not(eq(host(X2),index(pendack,host(X1)))),or(not(setIn(X3,alive)),or(not(eq(index(ldr,host(X3)),host(X3))),not(eq(index(status,host(X3)),norm))))))))) = true,
inference(equality_encoding,[status(esa)],[c111]) ).
cnf(t530,plain,
or(not(setIn(X1,alive)),or(not(elem(m_Ack(X1,X2),queue(host(X1)))),or(not(leq(nbr_proc,index(pendack,host(X1)))),or(not(eq(index(status,host(X1)),elec_2)),or(not(eq(host(X2),index(pendack,host(X1)))),or(not(setIn(X3,alive)),or(not(eq(index(ldr,host(X3)),host(X3))),not(eq(index(status,host(X3)),norm))))))))) = true,
inference(orient,[status(thm)],[t254]) ).
cnf(t611,plain,
true = or(not(true),or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(leq(nbr_proc,index(pendack,host(sk8)))),or(not(eq(index(status,host(sk8)),elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm))))))))),
inference(cp,[status(thm)],[t530,t585]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t1148,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t16944,plain,
true = or(false,or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(leq(nbr_proc,index(pendack,host(sk8)))),or(not(eq(index(status,host(sk8)),elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm))))))))),
inference(step,[status(thm)],[t611,t1148]) ).
cnf(t18,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t271,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t18]) ).
cnf(t16945,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(leq(nbr_proc,index(pendack,host(sk8)))),or(not(eq(index(status,host(sk8)),elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm)))))))),
inference(step,[status(thm)],[t16944,t271]) ).
cnf(t16946,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(leq(nbr_proc,nbr_proc)),or(not(eq(index(status,host(sk8)),elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm)))))))),
inference(step,[status(thm)],[t16945,t1305]) ).
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(t12,plain,
leq(X1,X1) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
cnf(t402,plain,
leq(X1,X1) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t16947,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(true),or(not(eq(index(status,host(sk8)),elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm)))))))),
inference(step,[status(thm)],[t16946,t402]) ).
cnf(t16948,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(false,or(not(eq(index(status,host(sk8)),elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm)))))))),
inference(step,[status(thm)],[t16947,t1148]) ).
cnf(t16949,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(index(status,host(sk8)),elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm))))))),
inference(step,[status(thm)],[t16948,t271]) ).
cnf(t16950,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(elec_2,elec_2)),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm))))))),
inference(step,[status(thm)],[t16949,t1208]) ).
cnf(t4,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t398,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t16951,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(true),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm))))))),
inference(step,[status(thm)],[t16950,t398]) ).
cnf(t16952,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(false,or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm))))))),
inference(step,[status(thm)],[t16951,t1148]) ).
cnf(t16953,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),index(pendack,host(sk8)))),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm)))))),
inference(step,[status(thm)],[t16952,t271]) ).
cnf(t16954,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm)))))),
inference(step,[status(thm)],[t16953,t1305]) ).
cnf(t14336,plain,
or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(not(setIn(X2,alive)),or(not(eq(index(ldr,host(X2)),host(X2))),not(eq(index(status,host(X2)),norm)))))) = true,
inference(orient,[status(thm)],[t16954]) ).
cnf(t14338,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(not(true),or(not(eq(index(ldr,host(sk6)),host(sk6))),not(eq(index(status,host(sk6)),norm)))))),
inference(cp,[status(thm)],[t14336,t641]) ).
cnf(t16955,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(false,or(not(eq(index(ldr,host(sk6)),host(sk6))),not(eq(index(status,host(sk6)),norm)))))),
inference(step,[status(thm)],[t14338,t1148]) ).
cnf(t16956,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(not(eq(index(ldr,host(sk6)),host(sk6))),not(eq(index(status,host(sk6)),norm))))),
inference(step,[status(thm)],[t16955,t271]) ).
cnf(t16957,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(not(eq(host(sk6),host(sk6))),not(eq(index(status,host(sk6)),norm))))),
inference(step,[status(thm)],[t16956,t1010]) ).
cnf(t16958,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(not(true),not(eq(index(status,host(sk6)),norm))))),
inference(step,[status(thm)],[t16957,t398]) ).
cnf(t16959,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),or(false,not(eq(index(status,host(sk6)),norm))))),
inference(step,[status(thm)],[t16958,t1148]) ).
cnf(t16960,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),not(eq(index(status,host(sk6)),norm)))),
inference(step,[status(thm)],[t16959,t271]) ).
cnf(t16961,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),not(eq(norm,norm)))),
inference(step,[status(thm)],[t16960,t1223]) ).
cnf(t16962,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),not(true))),
inference(step,[status(thm)],[t16961,t398]) ).
cnf(t16963,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),or(not(eq(host(X1),nbr_proc)),false)),
inference(step,[status(thm)],[t16962,t1148]) ).
cnf(t16,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t270,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t16]) ).
cnf(t16964,plain,
true = or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),not(eq(host(X1),nbr_proc))),
inference(step,[status(thm)],[t16963,t270]) ).
cnf(t14345,plain,
or(not(elem(m_Ack(sk8,X1),queue(host(sk8)))),not(eq(host(X1),nbr_proc))) = true,
inference(orient,[status(thm)],[t16964]) ).
cnf(t14346,plain,
true = or(not(elem(m_Ack(sk8,sk7),queue(host(sk8)))),not(eq(nbr_proc,nbr_proc))),
inference(cp,[status(thm)],[t14345,t1304]) ).
cnf(t16965,plain,
true = or(not(elem(m_Ack(sk8,sk7),queue(host(sk8)))),not(true)),
inference(step,[status(thm)],[t14346,t398]) ).
cnf(t16966,plain,
true = or(not(elem(m_Ack(sk8,sk7),queue(host(sk8)))),false),
inference(step,[status(thm)],[t16965,t1148]) ).
cnf(t16967,plain,
true = not(elem(m_Ack(sk8,sk7),queue(host(sk8)))),
inference(step,[status(thm)],[t16966,t270]) ).
cnf(t14347,plain,
not(elem(m_Ack(sk8,sk7),queue(host(sk8)))) = true,
inference(orient,[status(thm)],[t16967]) ).
cnf(t14348,plain,
false = ifeq(true,true,elem(m_Ack(sk8,sk7),queue(host(sk8))),false),
inference(cp,[status(thm)],[t851,t14347]) ).
cnf(t16968,plain,
false = elem(m_Ack(sk8,sk7),queue(host(sk8))),
inference(step,[status(thm)],[t14348,t256]) ).
cnf(t14350,plain,
elem(m_Ack(sk8,sk7),queue(host(sk8))) = false,
inference(orient,[status(thm)],[t16968]) ).
cnf(t16969,plain,
or(eq(m_Ack(sk8,sk7),m_Ack(sk5,sk4)),false) = true,
inference(step,[status(thm)],[t5202,t14350]) ).
cnf(t16970,plain,
eq(m_Ack(sk8,sk7),m_Ack(sk5,sk4)) = true,
inference(step,[status(thm)],[t16969,t270]) ).
cnf(t14378,plain,
eq(m_Ack(sk8,sk7),m_Ack(sk5,sk4)) = true,
inference(rw,[status(thm)],[t16970]) ).
cnf(t14379,plain,
eq(m_Ack(sk8,sk7),m_Ack(sk5,sk4)) = true,
inference(orient,[status(thm)],[t14378]) ).
cnf(t14380,plain,
m_Ack(sk5,sk4) = ifeq(true,true,m_Ack(sk8,sk7),m_Ack(sk5,sk4)),
inference(cp,[status(thm)],[t259,t14379]) ).
cnf(t16971,plain,
m_Ack(sk5,sk4) = m_Ack(sk8,sk7),
inference(step,[status(thm)],[t14380,t256]) ).
cnf(t14381,plain,
m_Ack(sk5,sk4) = m_Ack(sk8,sk7),
inference(orient,[status(thm)],[t16971]) ).
cnf(t14382,plain,
X1 = ifeq(m_Ack(sk8,sk7),m_Ack(X1,X2),sk5,X1),
inference(cp,[status(thm)],[t265,t14381]) ).
cnf(t14403,plain,
ifeq(m_Ack(sk8,sk7),m_Ack(X1,X2),sk5,X1) = X1,
inference(orient,[status(thm)],[t14382]) ).
cnf(t14404,plain,
sk8 = sk5,
inference(cp,[status(thm)],[t14403,t256]) ).
cnf(t14405,plain,
sk5 = sk8,
inference(orient,[status(thm)],[t14404]) ).
cnf(t16994,plain,
elem(m_Halt(sk8),queue(host(sk4))) = true,
inference(step,[status(thm)],[t1605,t14405]) ).
cnf(t14426,plain,
elem(m_Halt(sk8),queue(host(sk4))) = true,
inference(rw,[status(thm)],[t16994]) ).
cnf(t14560,plain,
elem(m_Halt(sk8),queue(host(sk4))) = true,
inference(orient,[status(thm)],[t14426]) ).
cnf(t14563,plain,
true = ifeq(true,true,leq(nbr_proc,host(sk6)),true),
inference(cp,[status(thm)],[t13388,t14560]) ).
cnf(t17055,plain,
true = leq(nbr_proc,host(sk6)),
inference(step,[status(thm)],[t14563,t256]) ).
cnf(t14575,plain,
leq(nbr_proc,host(sk6)) = true,
inference(orient,[status(thm)],[t17055]) ).
cnf(t14576,plain,
host(sk6) = ifeq(true,true,ifeq(leq(host(sk6),nbr_proc),true,nbr_proc,host(sk6)),host(sk6)),
inference(cp,[status(thm)],[t260,t14575]) ).
cnf(t17056,plain,
host(sk6) = ifeq(leq(host(sk6),nbr_proc),true,nbr_proc,host(sk6)),
inference(step,[status(thm)],[t14576,t256]) ).
cnf(t17057,plain,
host(sk6) = ifeq(true,true,nbr_proc,host(sk6)),
inference(step,[status(thm)],[t17056,t443]) ).
cnf(t17058,plain,
host(sk6) = nbr_proc,
inference(step,[status(thm)],[t17057,t256]) ).
cnf(t14604,plain,
host(sk6) = nbr_proc,
inference(orient,[status(thm)],[t17058]) ).
cnf(t17071,plain,
ifeq(host(sk4),nbr_proc,false,true) = true,
inference(step,[status(thm)],[t291,t14604]) ).
cnf(t14821,plain,
ifeq(host(sk4),nbr_proc,false,true) = true,
inference(rw,[status(thm)],[t17071]) ).
cnf(t14881,plain,
ifeq(host(sk4),nbr_proc,false,true) = true,
inference(orient,[status(thm)],[t14821]) ).
fof(f32,axiom,
! [X1,X2,Y1,Y2] :
( Y1 != Y2
=> m_Ack(X1,Y1) != m_Ack(X2,Y2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_32) ).
fof(f32_nnf,plain,
! [X1,X2,Y1,Y2] :
( m_Ack(X1,Y1) != m_Ack(X2,Y2)
| Y1 = Y2 ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [Y1,Y2,X1,X2] :
( m_Ack(X1,Y1) != m_Ack(X2,Y2)
| Y1 = Y2 ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c38,plain,
( m_Ack(X0,X2) != m_Ack(X1,X3)
| X2 = X3 ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t194,plain,
ifeq(m_Ack(X1,X2),m_Ack(X3,X4),X2,X4) = X4,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t264,plain,
ifeq(m_Ack(X1,X2),m_Ack(X3,X4),X2,X4) = X4,
inference(orient,[status(thm)],[t194]) ).
cnf(t16992,plain,
m_Ack(sk8,sk4) = m_Ack(sk8,sk7),
inference(step,[status(thm)],[t14381,t14405]) ).
cnf(t14424,plain,
m_Ack(sk8,sk4) = m_Ack(sk8,sk7),
inference(rw,[status(thm)],[t16992]) ).
cnf(t14484,plain,
m_Ack(sk8,sk4) = m_Ack(sk8,sk7),
inference(orient,[status(thm)],[t14424]) ).
cnf(t14485,plain,
X1 = ifeq(m_Ack(sk8,sk7),m_Ack(X2,X1),sk4,X1),
inference(cp,[status(thm)],[t264,t14484]) ).
cnf(t15057,plain,
ifeq(m_Ack(sk8,sk7),m_Ack(X1,X2),sk4,X2) = X2,
inference(orient,[status(thm)],[t14485]) ).
cnf(t15058,plain,
sk7 = sk4,
inference(cp,[status(thm)],[t15057,t256]) ).
cnf(t15059,plain,
sk4 = sk7,
inference(orient,[status(thm)],[t15058]) ).
cnf(t17155,plain,
ifeq(host(sk7),nbr_proc,false,true) = true,
inference(step,[status(thm)],[t14881,t15059]) ).
cnf(t17156,plain,
ifeq(nbr_proc,nbr_proc,false,true) = true,
inference(step,[status(thm)],[t17155,t1304]) ).
cnf(t17157,plain,
false = true,
inference(step,[status(thm)],[t17156,t256]) ).
cnf(t15063,plain,
false = true,
inference(rw,[status(thm)],[t17157]) ).
cnf(t15173,plain,
false = true,
inference(orient,[status(thm)],[t15063]) ).
fof(f1,axiom,
! [P,Q] :
( s(host(P)) = host(Q)
=> host(P) != host(Q) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_01) ).
fof(f1_nnf,plain,
! [P,Q] :
( host(P) != host(Q)
| s(host(P)) != host(Q) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [P,Q] :
( host(P) != host(Q)
| s(host(P)) != host(Q) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c2,plain,
( host(X0) != host(X1)
| s(host(X0)) != host(X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f5,axiom,
elec_1 != elec_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_05) ).
fof(f5_nnf,plain,
elec_1 != elec_2,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
elec_1 != elec_2,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c6,plain,
elec_1 != elec_2,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f6,axiom,
elec_1 != wait,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_06) ).
fof(f6_nnf,plain,
elec_1 != wait,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
elec_1 != wait,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c7,plain,
elec_1 != wait,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
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]) ).
fof(f8,axiom,
elec_2 != wait,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_08) ).
fof(f8_nnf,plain,
elec_2 != wait,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
elec_2 != wait,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c9,plain,
elec_2 != wait,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f9,axiom,
elec_2 != norm,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_09) ).
fof(f9_nnf,plain,
elec_2 != norm,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
elec_2 != norm,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c10,plain,
elec_2 != norm,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f10,axiom,
norm != wait,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
fof(f10_nnf,plain,
norm != wait,
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
norm != wait,
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c11,plain,
norm != wait,
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f11,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_11) ).
fof(f11_nnf,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Halt(Z),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c12,plain,
m_Ack(X0,X1) != m_Halt(X2),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
fof(f12,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_12) ).
fof(f12_nnf,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Down(Z),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c13,plain,
m_Ack(X0,X1) != m_Down(X2),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f13,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_NotNorm(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_13) ).
fof(f13_nnf,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_NotNorm(Z),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_NotNorm(Z),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c14,plain,
m_Ack(X0,X1) != m_NotNorm(X2),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
fof(f14,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_14) ).
fof(f14_nnf,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_Ldr(Z),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c15,plain,
m_Ack(X0,X1) != m_Ldr(X2),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f15,axiom,
! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(f15_nnf,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X,Y,Z] : m_Ack(X,Y) != m_NormQ(Z),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c16,plain,
m_Ack(X0,X1) != m_NormQ(X2),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
fof(f16,axiom,
! [X,Y] : m_NotNorm(X) != m_Halt(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_16) ).
fof(f16_nnf,plain,
! [X,Y] : m_NotNorm(X) != m_Halt(Y),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X,Y] : m_NotNorm(X) != m_Halt(Y),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c17,plain,
m_NotNorm(X0) != m_Halt(X1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f17,axiom,
! [X,Y] : m_Down(X) != m_Halt(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_17) ).
fof(f17_nnf,plain,
! [X,Y] : m_Down(X) != m_Halt(Y),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X,Y] : m_Down(X) != m_Halt(Y),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c18,plain,
m_Down(X0) != m_Halt(X1),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f18,axiom,
! [X,Y] : m_Down(X) != m_Ldr(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_18) ).
fof(f18_nnf,plain,
! [X,Y] : m_Down(X) != m_Ldr(Y),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X,Y] : m_Down(X) != m_Ldr(Y),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c19,plain,
m_Down(X0) != m_Ldr(X1),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f19,axiom,
! [X,Y] : m_Down(X) != m_NotNorm(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_19) ).
fof(f19_nnf,plain,
! [X,Y] : m_Down(X) != m_NotNorm(Y),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X,Y] : m_Down(X) != m_NotNorm(Y),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c20,plain,
m_Down(X0) != m_NotNorm(X1),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
fof(f20,axiom,
! [X,Y] : m_Down(X) != m_NormQ(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
fof(f20_nnf,plain,
! [X,Y] : m_Down(X) != m_NormQ(Y),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X,Y] : m_Down(X) != m_NormQ(Y),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c21,plain,
m_Down(X0) != m_NormQ(X1),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
fof(f21,axiom,
! [X,Y] : m_NormQ(X) != m_Halt(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
fof(f21_nnf,plain,
! [X,Y] : m_NormQ(X) != m_Halt(Y),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X,Y] : m_NormQ(X) != m_Halt(Y),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c22,plain,
m_NormQ(X0) != m_Halt(X1),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f22,axiom,
! [X,Y] : m_Ldr(X) != m_Halt(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_22) ).
fof(f22_nnf,plain,
! [X,Y] : m_Ldr(X) != m_Halt(Y),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X,Y] : m_Ldr(X) != m_Halt(Y),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c23,plain,
m_Ldr(X0) != m_Halt(X1),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
fof(f23,axiom,
! [X,Y] : m_Ldr(X) != m_NormQ(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_23) ).
fof(f23_nnf,plain,
! [X,Y] : m_Ldr(X) != m_NormQ(Y),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X,Y] : m_Ldr(X) != m_NormQ(Y),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c24,plain,
m_Ldr(X0) != m_NormQ(X1),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
fof(f24,axiom,
! [X,Y] : m_Ldr(X) != m_NotNorm(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_24) ).
fof(f24_nnf,plain,
! [X,Y] : m_Ldr(X) != m_NotNorm(Y),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X,Y] : m_Ldr(X) != m_NotNorm(Y),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c25,plain,
m_Ldr(X0) != m_NotNorm(X1),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f25,axiom,
! [X,Y] : m_NormQ(X) != m_NotNorm(Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_25) ).
fof(f25_nnf,plain,
! [X,Y] : m_NormQ(X) != m_NotNorm(Y),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [X,Y] : m_NormQ(X) != m_NotNorm(Y),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c26,plain,
m_NormQ(X0) != m_NotNorm(X1),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f34,axiom,
~ setIn(nil,alive),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_34) ).
fof(f34_nnf,plain,
~ setIn(nil,alive),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
~ setIn(nil,alive),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c40,plain,
~ setIn(nil,alive),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
fof(f41,axiom,
! [X,Q] : q_nil != cons(X,Q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_41) ).
fof(f41_nnf,plain,
! [X,Q] : q_nil != cons(X,Q),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X,Q] : q_nil != cons(X,Q),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c47,plain,
q_nil != cons(X0,X1),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f42,axiom,
! [Y,Q] : q_nil != snoc(Q,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_42) ).
fof(f42_nnf,plain,
! [Y,Q] : q_nil != snoc(Q,Y),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [Q,Y] : q_nil != snoc(Q,Y),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c48,plain,
q_nil != snoc(X1,X0),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
fof(f45,axiom,
! [X] : ~ elem(X,q_nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_45) ).
fof(f45_nnf,plain,
! [X] : ~ elem(X,q_nil),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [X] : ~ elem(X,q_nil),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c51,plain,
~ elem(X0,q_nil),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
fof(f58,axiom,
! [X] : ~ leq(s(X),X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_58) ).
fof(f58_nnf,plain,
! [X] : ~ leq(s(X),X),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
! [X] : ~ leq(s(X),X),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c83,plain,
~ leq(s(X0),X0),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
fof(f65,axiom,
! [X] : ~ setIn(X,setEmpty),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_65) ).
fof(f65_nnf,plain,
! [X] : ~ setIn(X,setEmpty),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [X] : ~ setIn(X,setEmpty),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c95,plain,
~ setIn(X0,setEmpty),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(c97,plain,
( ~ setIn(X4,alive)
| ~ elem(m_Down(X4),queue(host(X3))) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c98,plain,
( ~ leq(host(X3),host(X4))
| ~ elem(m_Ldr(X4),queue(host(X3))) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c99,plain,
( ~ leq(host(X3),host(X5))
| ~ elem(m_Ack(X5,X3),queue(host(X4))) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c103,plain,
( ~ elem(m_Ack(X3,X4),queue(host(X3)))
| index(status,host(X4)) != elec_1
| ~ setIn(X4,alive) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c104,plain,
( ~ elem(m_Ack(X4,X3),queue(host(X4)))
| index(status,host(X4)) != elec_1
| ~ setIn(X4,alive) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c107,plain,
( ~ setIn(X5,alive)
| host(X5) != host(X3)
| ~ elem(m_Ack(X5,X4),queue(host(X5)))
| ~ elem(m_Down(X3),queue(host(X4))) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c108,plain,
( ~ setIn(host(X5),index(down,host(X4)))
| host(X4) != host(X3)
| ~ elem(m_Ack(X5,X3),queue(host(X5)))
| ~ setIn(X5,alive)
| ~ setIn(X4,alive) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(c116,plain,
host(sk4) != host(sk8),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26,c40,c47,c48,c51,c83,c95,c97,c98,c99,c103,c104,c107,c108,c111,c114,c116]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t15173]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV457+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 19:49:41 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 169.43/21.92 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 169.43/21.92 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------