%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV462+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Sun Sep 27 09:02:27 AM UTC 2026
% Result : Theorem 73.35s 9.90s
% Output : CNFRefutation 73.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 12
% Syntax : Number of formulae : 122 ( 40 unt; 0 def)
% Number of atoms : 551 ( 267 equ)
% Maximal formula atoms : 88 ( 4 avg)
% Number of connectives : 742 ( 313 ~; 253 |; 125 &)
% ( 5 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 18 con; 0-2 aty)
% Number of variables : 237 ( 35 sgn 117 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_04,axiom,
! [X0] : leq(host(X0),'nbr$uproc') ).
fof(axiom_11,axiom,
! [X0,X1,X2] : 'm$uAck'(X0,X1) != 'm$uHalt'(X2) ).
fof(axiom_12,axiom,
! [X0,X1,X2] : 'm$uAck'(X0,X1) != 'm$uDown'(X2) ).
fof(axiom_31,axiom,
! [X0,X1,X2,X3] :
( X0 != X1
=> 'm$uAck'(X0,X2) != 'm$uAck'(X1,X3) ) ).
fof(axiom_32,axiom,
! [X0,X1,X2,X3] :
( X2 != X3
=> 'm$uAck'(X0,X2) != 'm$uAck'(X1,X3) ) ).
fof(axiom_46,axiom,
! [X0,X1,X2] :
( elem(X0,cons(X1,X2))
<=> ( elem(X0,X2)
| X0 = X1 ) ) ).
fof(axiom_47,axiom,
! [X0,X1,X2] :
( elem(X0,snoc(X2,X1))
<=> ( elem(X0,X2)
| X0 = X1 ) ) ).
fof(axiom_48,axiom,
! [X0] :
( pidElem(X0)
<=> ? [X1] :
( X0 = 'm$uDown'(X1)
| X0 = 'm$uHalt'(X1) ) ) ).
fof(axiom_59,axiom,
! [X0] : leq(X0,X0) ).
fof(axiom_61,axiom,
! [X0,X1] :
( ( leq(X1,X0)
& leq(X0,X1) )
<=> X0 = X1 ) ).
fof(axiom_64,axiom,
! [X0,X1] :
( leq(X0,s(X1))
<=> ( leq(X0,X1)
| X0 = s(X1) ) ) ).
fof(conj,conjecture,
! [X0,X1,X2] :
( ( queue(host(X1)) = cons('m$uHalt'(X2),X0)
& ! [X3,X4,X6,X5] :
( ( host(X6) = s(index(pendack,host(X5)))
& host(X4) = index(pendack,host(X5))
& index(status,host(X5)) = 'elec$u2'
& leq('nbr$uproc',s(index(pendack,host(X5))))
& elem('m$uDown'(X6),queue(host(X5)))
& elem('m$uAck'(X5,X4),queue(host(X5)))
& setIn(X5,alive) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) )
& ! [X3,X4,X6,X5] :
( ( index(status,host(X5)) = 'elec$u1'
& host(X5) = 'nbr$uproc'
& host(X5) = host(X4)
& elem('m$uDown'(X6),queue(host(X5)))
& ! [X7] :
( ( leq(s(zero),X7)
& ~ leq(host(X5),X7) )
=> ( X7 = host(X6)
| setIn(X7,index(down,host(X5))) ) ) )
=> ~ ( elem('m$uDown'(X4),queue(host(X3)))
& setIn(X3,alive) ) )
& ! [X3,X4,X5] :
( ( index(status,host(X5)) = 'elec$u2'
& elem('m$uHalt'(X5),queue(host(X4)))
& setIn(X5,alive)
& ~ leq(index(pendack,host(X5)),host(X3)) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) )
& ! [X3,X4] :
( ( index(status,host(X4)) = 'elec$u2'
& index(status,host(X3)) = 'elec$u2'
& setIn(X4,alive)
& setIn(X3,alive)
& ~ leq(host(X3),host(X4)) )
=> ~ leq(index(pendack,host(X3)),index(pendack,host(X4))) )
& ! [X3,X4,X5] :
( ( index(status,host(X5)) = 'elec$u2'
& index(status,host(X3)) = 'elec$u2'
& host(X5) = host(X4)
& setIn(X5,alive)
& setIn(X3,alive) )
=> ~ elem('m$uAck'(X3,X4),queue(host(X3))) )
& ! [X3,X4,X5] :
( ( host(X4) = host(X3)
& elem('m$uDown'(X4),queue(host(X5)))
& setIn(X5,alive) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) )
& ! [X3,X4] :
( ( index(status,host(X4)) = 'elec$u2'
& index(status,host(X3)) = 'elec$u2'
& setIn(X4,alive)
& setIn(X3,alive)
& ~ leq(host(X3),host(X4)) )
=> leq(index(pendack,host(X4)),host(X3)) )
& ! [X3] :
( ( setIn(X3,alive)
& ( index(status,host(X3)) = 'elec$u2'
| index(status,host(X3)) = 'elec$u1' ) )
=> index(elid,host(X3)) = X3 )
& ! [X3,X4] :
( ( index(status,host(X4)) = 'elec$u1'
& setIn(X4,alive) )
=> ~ elem('m$uAck'(X4,X3),queue(host(X4))) )
& ! [X3,X4] :
( ( elem('m$uAck'(X4,X3),queue(host(X4)))
& setIn(X4,alive) )
=> leq(host(X3),index(pendack,host(X4))) )
& ! [X3,X4] :
( ( host(X4) = host(X3)
& X4 != X3 )
=> ( ~ setIn(X4,alive)
| ~ setIn(X3,alive) ) )
& ! [X3,X4,X5] :
( elem('m$uAck'(X5,X3),queue(host(X4)))
=> ~ leq(host(X3),host(X5)) )
& ! [X3,X4] :
( elem('m$uHalt'(X4),queue(host(X3)))
=> ~ leq(host(X3),host(X4)) )
& ! [X3,X4] :
( elem('m$uDown'(X4),queue(host(X3)))
=> host(X4) != host(X3) )
& ! [X3,X4] :
( elem('m$uLdr'(X4),queue(host(X3)))
=> ~ leq(host(X3),host(X4)) ) )
=> ( setIn(X1,alive)
=> ! [X3] :
( host(X1) != host(X3)
=> ! [X4,X8,X9] :
( host(X2) = host(X9)
=> ( host(X1) != host(X9)
=> ( ( host(X8) = s(index(pendack,host(X9)))
& host(X4) = index(pendack,host(X9))
& index(status,host(X9)) = 'elec$u2'
& elem('m$uAck'(X9,X4),snoc(queue(host(X9)),'m$uAck'(X2,X1)))
& elem('m$uDown'(X8),snoc(queue(host(X9)),'m$uAck'(X2,X1)))
& leq('nbr$uproc',s(index(pendack,host(X9))))
& setIn(X9,alive) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) ) ) ) ) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0,X1,X2] :
( ( queue(host(X1)) = cons('m$uHalt'(X2),X0)
& ! [X3,X4,X6,X5] :
( ( host(X6) = s(index(pendack,host(X5)))
& host(X4) = index(pendack,host(X5))
& index(status,host(X5)) = 'elec$u2'
& leq('nbr$uproc',s(index(pendack,host(X5))))
& elem('m$uDown'(X6),queue(host(X5)))
& elem('m$uAck'(X5,X4),queue(host(X5)))
& setIn(X5,alive) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) )
& ! [X3,X4,X6,X5] :
( ( index(status,host(X5)) = 'elec$u1'
& host(X5) = 'nbr$uproc'
& host(X5) = host(X4)
& elem('m$uDown'(X6),queue(host(X5)))
& ! [X7] :
( ( leq(s(zero),X7)
& ~ leq(host(X5),X7) )
=> ( X7 = host(X6)
| setIn(X7,index(down,host(X5))) ) ) )
=> ~ ( elem('m$uDown'(X4),queue(host(X3)))
& setIn(X3,alive) ) )
& ! [X3,X4,X5] :
( ( index(status,host(X5)) = 'elec$u2'
& elem('m$uHalt'(X5),queue(host(X4)))
& setIn(X5,alive)
& ~ leq(index(pendack,host(X5)),host(X3)) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) )
& ! [X3,X4] :
( ( index(status,host(X4)) = 'elec$u2'
& index(status,host(X3)) = 'elec$u2'
& setIn(X4,alive)
& setIn(X3,alive)
& ~ leq(host(X3),host(X4)) )
=> ~ leq(index(pendack,host(X3)),index(pendack,host(X4))) )
& ! [X3,X4,X5] :
( ( index(status,host(X5)) = 'elec$u2'
& index(status,host(X3)) = 'elec$u2'
& host(X5) = host(X4)
& setIn(X5,alive)
& setIn(X3,alive) )
=> ~ elem('m$uAck'(X3,X4),queue(host(X3))) )
& ! [X3,X4,X5] :
( ( host(X4) = host(X3)
& elem('m$uDown'(X4),queue(host(X5)))
& setIn(X5,alive) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) )
& ! [X3,X4] :
( ( index(status,host(X4)) = 'elec$u2'
& index(status,host(X3)) = 'elec$u2'
& setIn(X4,alive)
& setIn(X3,alive)
& ~ leq(host(X3),host(X4)) )
=> leq(index(pendack,host(X4)),host(X3)) )
& ! [X3] :
( ( setIn(X3,alive)
& ( index(status,host(X3)) = 'elec$u2'
| index(status,host(X3)) = 'elec$u1' ) )
=> index(elid,host(X3)) = X3 )
& ! [X3,X4] :
( ( index(status,host(X4)) = 'elec$u1'
& setIn(X4,alive) )
=> ~ elem('m$uAck'(X4,X3),queue(host(X4))) )
& ! [X3,X4] :
( ( elem('m$uAck'(X4,X3),queue(host(X4)))
& setIn(X4,alive) )
=> leq(host(X3),index(pendack,host(X4))) )
& ! [X3,X4] :
( ( host(X4) = host(X3)
& X4 != X3 )
=> ( ~ setIn(X4,alive)
| ~ setIn(X3,alive) ) )
& ! [X3,X4,X5] :
( elem('m$uAck'(X5,X3),queue(host(X4)))
=> ~ leq(host(X3),host(X5)) )
& ! [X3,X4] :
( elem('m$uHalt'(X4),queue(host(X3)))
=> ~ leq(host(X3),host(X4)) )
& ! [X3,X4] :
( elem('m$uDown'(X4),queue(host(X3)))
=> host(X4) != host(X3) )
& ! [X3,X4] :
( elem('m$uLdr'(X4),queue(host(X3)))
=> ~ leq(host(X3),host(X4)) ) )
=> ( setIn(X1,alive)
=> ! [X3] :
( host(X1) != host(X3)
=> ! [X4,X8,X9] :
( host(X2) = host(X9)
=> ( host(X1) != host(X9)
=> ( ( host(X8) = s(index(pendack,host(X9)))
& host(X4) = index(pendack,host(X9))
& index(status,host(X9)) = 'elec$u2'
& elem('m$uAck'(X9,X4),snoc(queue(host(X9)),'m$uAck'(X2,X1)))
& elem('m$uDown'(X8),snoc(queue(host(X9)),'m$uAck'(X2,X1)))
& leq('nbr$uproc',s(index(pendack,host(X9))))
& setIn(X9,alive) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) ) ) ) ) ) ),
inference(negate_conjecture,[status(cth)],[conj]) ).
cnf(c5,plain,
leq(host(X0),'nbr$uproc'),
inference(clausification,[status(esa)],[axiom_04]) ).
cnf(c12,plain,
'm$uAck'(X0,X1) != 'm$uHalt'(X2),
inference(clausification,[status(esa)],[axiom_11]) ).
cnf(c13,plain,
'm$uAck'(X0,X1) != 'm$uDown'(X2),
inference(clausification,[status(esa)],[axiom_12]) ).
cnf(c37,plain,
( 'm$uAck'(X0,X2) != 'm$uAck'(X1,X3)
| X0 = X1 ),
inference(clausification,[status(esa)],[axiom_31]) ).
cnf(c38,plain,
( 'm$uAck'(X2,X0) != 'm$uAck'(X3,X1)
| X0 = X1 ),
inference(clausification,[status(esa)],[axiom_32]) ).
cnf(c53,plain,
( X0 != X1
| elem(X0,cons(X1,X2)) ),
inference(clausification,[status(esa)],[axiom_46]) ).
cnf(c55,plain,
( elem(X0,X1)
| X0 = X2
| ~ elem(X0,snoc(X1,X2)) ),
inference(clausification,[status(esa)],[axiom_47]) ).
cnf(c58,plain,
( X0 = 'm$uDown'(sK87(X0))
| X0 = 'm$uHalt'(sK87(X0))
| ~ pidElem(X0) ),
inference(clausification,[status(esa)],[axiom_48]) ).
cnf(c60,plain,
( X0 != 'm$uDown'(X1)
| pidElem(X0) ),
inference(clausification,[status(esa)],[axiom_48]) ).
cnf(c88,plain,
leq(X0,X0),
inference(clausification,[status(esa)],[axiom_59]) ).
cnf(c90,plain,
( X0 = X1
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(clausification,[status(esa)],[axiom_61]) ).
cnf(c96,plain,
( leq(X0,X1)
| X0 = s(X1)
| ~ leq(X0,s(X1)) ),
inference(clausification,[status(esa)],[axiom_64]) ).
cnf(c110,plain,
( ~ elem('m$uDown'(X0),queue(host(X2)))
| ~ setIn(X2,alive)
| ~ setIn(X1,alive)
| index(status,host(X1)) != norm
| index(ldr,host(X1)) != host(X1)
| host(X0) != host(X1) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c113,plain,
( ~ setIn(X1,alive)
| index(status,host(X1)) != norm
| index(status,host(X0)) != 'elec$u2'
| ~ setIn(X0,alive)
| index(ldr,host(X1)) != host(X1)
| ~ elem('m$uHalt'(X0),queue(host(X2)))
| leq(index(pendack,host(X0)),host(X1)) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c118,plain,
( host(X3) != s(index(pendack,host(X0)))
| ~ elem('m$uDown'(X3),queue(host(X0)))
| index(status,host(X0)) != 'elec$u2'
| ~ elem('m$uAck'(X0,X1),queue(host(X0)))
| ~ setIn(X0,alive)
| index(ldr,host(X2)) != host(X2)
| index(status,host(X2)) != norm
| ~ setIn(X2,alive)
| host(X1) != index(pendack,host(X0))
| ~ leq('nbr$uproc',s(index(pendack,host(X0)))) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c119,plain,
queue(host(sK125)) = cons('m$uHalt'(sK126),sK124),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c121,plain,
host(sK125) != host(sK165),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c122,plain,
host(sK126) = host(sK168),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c124,plain,
setIn(sK168,alive),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c125,plain,
leq('nbr$uproc',s(index(pendack,host(sK168)))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c126,plain,
elem('m$uDown'(sK167),snoc(queue(host(sK168)),'m$uAck'(sK126,sK125))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c127,plain,
elem('m$uAck'(sK168,sK166),snoc(queue(host(sK168)),'m$uAck'(sK126,sK125))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c128,plain,
index(status,host(sK168)) = 'elec$u2',
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c129,plain,
host(sK166) = index(pendack,host(sK168)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c130,plain,
host(sK167) = s(index(pendack,host(sK168))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c131,plain,
setIn(sK165,alive),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c132,plain,
index(ldr,host(sK165)) = host(sK165),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c133,plain,
index(status,host(sK165)) = norm,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ pidElem(X0)
| X0 = 'm$uHalt'(sK87(X0))
| 'm$uAck'(X1,X2) != X0 ),
inference(superposition,[status(thm)],[c58,c13]) ).
cnf(d1,plain,
( ~ pidElem('m$uAck'(X0,X1))
| 'm$uAck'(X0,X1) = 'm$uHalt'(sK87('m$uAck'(X0,X1))) ),
inference(equality_resolution,[status(thm)],[d0]) ).
cnf(d2,plain,
~ pidElem('m$uAck'(X0,X1)),
inference(resolution,[status(thm)],[c12,d1]) ).
cnf(d3,plain,
( elem('m$uDown'(sK167),queue(host(sK168)))
| 'm$uDown'(sK167) = 'm$uAck'(sK126,sK125) ),
inference(resolution,[status(thm)],[c55,c126]) ).
cnf(d4,plain,
host(sK167) = s(host(sK166)),
inference(demodulation,[status(thm)],[c130,c129]) ).
cnf(d5,plain,
( ~ leq('nbr$uproc',s(index(pendack,host(sK168))))
| ~ setIn(X2,alive)
| ~ setIn(sK168,alive)
| ~ elem('m$uDown'(X0),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X1),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| index(status,host(X2)) != norm
| index(status,host(sK168)) != 'elec$u2'
| host(X1) != index(pendack,host(sK168))
| host(X0) != s(host(sK166)) ),
inference(superposition,[status(thm)],[c129,c118]) ).
cnf(d6,plain,
( ~ leq('nbr$uproc',s(index(pendack,host(sK168))))
| ~ setIn(sK168,alive)
| ~ setIn(X2,alive)
| ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| index(status,host(sK168)) != 'elec$u2'
| index(status,host(X2)) != norm
| host(X1) != s(host(sK166))
| host(X0) != host(sK166) ),
inference(demodulation,[status(thm)],[d5,c129]) ).
cnf(d7,plain,
( ~ leq('nbr$uproc',s(index(pendack,host(sK168))))
| ~ setIn(sK168,alive)
| ~ setIn(X2,alive)
| ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| index(status,host(sK168)) != 'elec$u2'
| index(status,host(X2)) != norm
| host(X1) != host(sK167)
| host(X0) != host(sK166) ),
inference(demodulation,[status(thm)],[d6,d4]) ).
cnf(d8,plain,
( ~ leq('nbr$uproc',s(index(pendack,host(sK168))))
| ~ setIn(sK168,alive)
| ~ setIn(X2,alive)
| ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| 'elec$u2' != 'elec$u2'
| index(status,host(X2)) != norm
| host(X1) != host(sK167)
| host(X0) != host(sK166) ),
inference(demodulation,[status(thm)],[d7,c128]) ).
cnf(d9,plain,
( ~ leq('nbr$uproc',s(host(sK166)))
| ~ setIn(sK168,alive)
| ~ setIn(X2,alive)
| ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| 'elec$u2' != 'elec$u2'
| index(status,host(X2)) != norm
| host(X1) != host(sK167)
| host(X0) != host(sK166) ),
inference(demodulation,[status(thm)],[d8,c129]) ).
cnf(d10,plain,
( ~ leq('nbr$uproc',host(sK167))
| ~ setIn(sK168,alive)
| ~ setIn(X2,alive)
| ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| 'elec$u2' != 'elec$u2'
| index(status,host(X2)) != norm
| host(X1) != host(sK167)
| host(X0) != host(sK166) ),
inference(demodulation,[status(thm)],[d9,d4]) ).
cnf(d11,plain,
( ~ leq('nbr$uproc',host(sK167))
| ~ setIn(X2,alive)
| ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| 'elec$u2' != 'elec$u2'
| index(status,host(X2)) != norm
| host(X1) != host(sK167)
| host(X0) != host(sK166) ),
inference(resolution,[status(thm)],[c124,d10]) ).
cnf(d12,plain,
leq('nbr$uproc',s(host(sK166))),
inference(demodulation,[status(thm)],[c125,c129]) ).
cnf(d13,plain,
leq('nbr$uproc',host(sK167)),
inference(demodulation,[status(thm)],[d12,d4]) ).
cnf(d14,plain,
( ~ setIn(X2,alive)
| ~ elem('m$uDown'(X0),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X1),queue(host(sK168)))
| index(ldr,host(X2)) != host(X2)
| index(status,host(X2)) != norm
| 'elec$u2' != 'elec$u2'
| host(X1) != host(sK166)
| host(X0) != host(sK167) ),
inference(resolution,[status(thm)],[d13,d11]) ).
cnf(d15,plain,
( ~ setIn(sK165,alive)
| ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| index(status,host(sK165)) != norm
| 'elec$u2' != 'elec$u2'
| host(X1) != host(sK167)
| host(X0) != host(sK166)
| host(sK165) != host(sK165) ),
inference(superposition,[status(thm)],[c132,d14]) ).
cnf(d16,plain,
( ~ setIn(sK165,alive)
| ~ elem('m$uDown'(X0),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X1),queue(host(sK168)))
| norm != norm
| 'elec$u2' != 'elec$u2'
| host(sK165) != host(sK165)
| host(X1) != host(sK166)
| host(X0) != host(sK167) ),
inference(demodulation,[status(thm)],[d15,c133]) ).
cnf(d17,plain,
( ~ elem('m$uDown'(X0),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X1),queue(host(sK168)))
| norm != norm
| 'elec$u2' != 'elec$u2'
| host(sK165) != host(sK165)
| host(X1) != host(sK166)
| host(X0) != host(sK167) ),
inference(resolution,[status(thm)],[c131,d16]) ).
cnf(d18,plain,
( ~ elem('m$uDown'(X1),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,X0),queue(host(sK168)))
| norm != norm
| 'elec$u2' != 'elec$u2'
| host(X1) != host(sK167)
| host(X0) != host(sK166) ),
inference(equality_resolution,[status(thm)],[d17]) ).
cnf(d19,plain,
( ~ elem('m$uDown'(X0),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,sK166),queue(host(sK168)))
| norm != norm
| 'elec$u2' != 'elec$u2'
| host(X0) != host(sK167) ),
inference(equality_resolution,[status(thm)],[d18]) ).
cnf(d20,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,sK166),queue(host(sK168)))
| norm != norm
| 'elec$u2' != 'elec$u2' ),
inference(equality_resolution,[status(thm)],[d19]) ).
cnf(d21,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,sK166),queue(host(sK168)))
| 'elec$u2' != 'elec$u2' ),
inference(equality_resolution,[status(thm)],[d20]) ).
cnf(d22,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,sK166),queue(host(sK168))) ),
inference(equality_resolution,[status(thm)],[d21]) ).
cnf(d23,plain,
( elem('m$uAck'(sK168,sK166),queue(host(sK168)))
| 'm$uAck'(sK168,sK166) = 'm$uAck'(sK126,sK125) ),
inference(resolution,[status(thm)],[c55,c127]) ).
cnf(d24,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| 'm$uAck'(sK168,sK166) = 'm$uAck'(sK126,sK125) ),
inference(resolution,[status(thm)],[d23,d22]) ).
cnf(d25,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| sK125 = X1
| 'm$uAck'(sK168,sK166) != 'm$uAck'(X0,X1) ),
inference(superposition,[status(thm)],[d24,c38]) ).
cnf(d26,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| sK125 = sK166 ),
inference(equality_resolution,[status(thm)],[d25]) ).
cnf(d27,plain,
( 'm$uDown'(sK167) = 'm$uAck'(sK126,sK125)
| sK125 = sK166 ),
inference(resolution,[status(thm)],[d26,d3]) ).
cnf(d28,plain,
( sK125 = sK166
| 'm$uDown'(sK167) != 'm$uDown'(X0) ),
inference(superposition,[status(thm)],[d27,c13]) ).
cnf(d29,plain,
sK125 = sK166,
inference(equality_resolution,[status(thm)],[d28]) ).
cnf(d30,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| sK126 = X0
| 'm$uAck'(sK168,sK166) != 'm$uAck'(X0,X1) ),
inference(superposition,[status(thm)],[d24,c37]) ).
cnf(d31,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| sK126 = X0
| 'm$uAck'(sK168,sK125) != 'm$uAck'(X0,X1) ),
inference(demodulation,[status(thm)],[d30,d29]) ).
cnf(d32,plain,
( ~ elem('m$uDown'(sK167),queue(host(sK168)))
| sK126 = sK168 ),
inference(equality_resolution,[status(thm)],[d31]) ).
cnf(d33,plain,
( 'm$uDown'(sK167) = 'm$uAck'(sK126,sK125)
| sK126 = sK168 ),
inference(resolution,[status(thm)],[d32,d3]) ).
cnf(d34,plain,
( sK126 = sK168
| 'm$uDown'(sK167) != 'm$uDown'(X0) ),
inference(superposition,[status(thm)],[d33,c13]) ).
cnf(d35,plain,
sK126 = sK168,
inference(equality_resolution,[status(thm)],[d34]) ).
cnf(d36,plain,
( leq(index(pendack,host(X0)),host(sK165))
| ~ setIn(X0,alive)
| ~ setIn(sK165,alive)
| ~ elem('m$uHalt'(X0),queue(host(X1)))
| index(status,host(X0)) != 'elec$u2'
| index(status,host(sK165)) != norm
| host(sK165) != host(sK165) ),
inference(superposition,[status(thm)],[c132,c113]) ).
cnf(d37,plain,
( leq(index(pendack,host(X0)),host(sK165))
| ~ setIn(sK165,alive)
| ~ setIn(X0,alive)
| ~ elem('m$uHalt'(X0),queue(host(X1)))
| norm != norm
| index(status,host(X0)) != 'elec$u2'
| host(sK165) != host(sK165) ),
inference(demodulation,[status(thm)],[d36,c133]) ).
cnf(d38,plain,
( leq(index(pendack,host(X0)),host(sK165))
| ~ setIn(X0,alive)
| ~ elem('m$uHalt'(X0),queue(host(X1)))
| norm != norm
| index(status,host(X0)) != 'elec$u2'
| host(sK165) != host(sK165) ),
inference(resolution,[status(thm)],[c131,d37]) ).
cnf(d39,plain,
( leq(index(pendack,host(sK126)),host(sK165))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| norm != norm
| host(sK165) != host(sK165)
| index(status,host(sK168)) != 'elec$u2' ),
inference(superposition,[status(thm)],[c122,d38]) ).
cnf(d40,plain,
( leq(index(pendack,host(sK126)),host(sK165))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK165) != host(sK165) ),
inference(demodulation,[status(thm)],[d39,c128]) ).
cnf(d41,plain,
( leq(index(pendack,host(sK168)),host(sK165))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK165) != host(sK165) ),
inference(demodulation,[status(thm)],[d40,c122]) ).
cnf(d42,plain,
( leq(host(sK166),host(sK165))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK165) != host(sK165) ),
inference(demodulation,[status(thm)],[d41,c129]) ).
cnf(d43,plain,
( leq(host(sK166),host(sK165))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm ),
inference(equality_resolution,[status(thm)],[d42]) ).
cnf(d44,plain,
( leq(host(sK166),host(sK165))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2' ),
inference(equality_resolution,[status(thm)],[d43]) ).
cnf(d45,plain,
( leq(host(sK166),host(sK165))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0))) ),
inference(equality_resolution,[status(thm)],[d44]) ).
cnf(d46,plain,
elem(X0,cons(X0,X1)),
inference(equality_resolution,[status(thm)],[c53]) ).
cnf(d47,plain,
elem('m$uHalt'(sK126),queue(host(sK125))),
inference(superposition,[status(thm)],[c119,d46]) ).
cnf(d48,plain,
( leq(host(sK166),host(sK165))
| ~ setIn(sK126,alive) ),
inference(resolution,[status(thm)],[d47,d45]) ).
cnf(d49,plain,
( leq(host(sK125),host(sK165))
| ~ setIn(sK126,alive) ),
inference(demodulation,[status(thm)],[d48,d29]) ).
cnf(d50,plain,
( leq(host(sK125),host(sK165))
| ~ setIn(sK168,alive) ),
inference(demodulation,[status(thm)],[d49,d35]) ).
cnf(d51,plain,
leq(host(sK125),host(sK165)),
inference(resolution,[status(thm)],[c124,d50]) ).
cnf(d52,plain,
( ~ leq(host(sK165),host(sK125))
| host(sK125) = host(sK165) ),
inference(resolution,[status(thm)],[d51,c90]) ).
cnf(d53,plain,
~ leq(host(sK165),host(sK125)),
inference(resolution,[status(thm)],[c121,d52]) ).
cnf(d54,plain,
( ~ leq(host(sK167),'nbr$uproc')
| 'nbr$uproc' = host(sK167) ),
inference(resolution,[status(thm)],[c90,d13]) ).
cnf(d55,plain,
'nbr$uproc' = host(sK167),
inference(resolution,[status(thm)],[c5,d54]) ).
cnf(d56,plain,
host(sK167) = s(host(sK125)),
inference(demodulation,[status(thm)],[d4,d29]) ).
cnf(d57,plain,
'nbr$uproc' = s(host(sK125)),
inference(demodulation,[status(thm)],[d56,d55]) ).
cnf(d58,plain,
( leq(X0,host(sK125))
| X0 = s(host(sK125))
| ~ leq(X0,host(sK167)) ),
inference(superposition,[status(thm)],[d56,c96]) ).
cnf(d59,plain,
( ~ leq(X0,host(sK167))
| leq(X0,host(sK125))
| X0 = 'nbr$uproc' ),
inference(demodulation,[status(thm)],[d58,d57]) ).
cnf(d60,plain,
( ~ leq(X0,'nbr$uproc')
| leq(X0,host(sK125))
| X0 = 'nbr$uproc' ),
inference(demodulation,[status(thm)],[d59,d55]) ).
cnf(d61,plain,
( ~ leq(host(sK165),'nbr$uproc')
| host(sK165) = 'nbr$uproc' ),
inference(resolution,[status(thm)],[d60,d53]) ).
cnf(d62,plain,
host(sK165) = 'nbr$uproc',
inference(resolution,[status(thm)],[c5,d61]) ).
cnf(d63,plain,
( ~ setIn(sK165,alive)
| ~ setIn(X1,alive)
| ~ elem('m$uDown'(X0),queue(host(X1)))
| index(status,host(sK165)) != norm
| host(X0) != host(sK165)
| host(sK165) != host(sK165) ),
inference(superposition,[status(thm)],[c132,c110]) ).
cnf(d64,plain,
( ~ setIn(sK165,alive)
| ~ setIn(X1,alive)
| ~ elem('m$uDown'(X0),queue(host(X1)))
| norm != norm
| host(sK165) != host(sK165)
| host(X0) != host(sK165) ),
inference(demodulation,[status(thm)],[d63,c133]) ).
cnf(d65,plain,
( ~ setIn(X1,alive)
| ~ elem('m$uDown'(X0),queue(host(X1)))
| norm != norm
| host(sK165) != host(sK165)
| host(X0) != host(sK165) ),
inference(resolution,[status(thm)],[c131,d64]) ).
cnf(d66,plain,
( ~ setIn(X1,alive)
| ~ elem('m$uDown'(X0),queue(host(X1)))
| norm != norm
| host(X0) != host(sK165) ),
inference(equality_resolution,[status(thm)],[d65]) ).
cnf(d67,plain,
( ~ setIn(X0,alive)
| ~ elem('m$uDown'(sK167),queue(host(X0)))
| norm != norm
| 'nbr$uproc' != host(sK165) ),
inference(superposition,[status(thm)],[d55,d66]) ).
cnf(d68,plain,
( ~ setIn(X0,alive)
| ~ elem('m$uDown'(sK167),queue(host(X0)))
| norm != norm
| 'nbr$uproc' != 'nbr$uproc' ),
inference(demodulation,[status(thm)],[d67,d62]) ).
cnf(d69,plain,
( ~ leq('nbr$uproc',host(X0))
| host(X0) = 'nbr$uproc' ),
inference(resolution,[status(thm)],[c90,c5]) ).
cnf(d70,plain,
( host(sK167) = 'nbr$uproc'
| ~ leq('nbr$uproc','nbr$uproc') ),
inference(superposition,[status(thm)],[d55,d69]) ).
cnf(d71,plain,
( ~ leq('nbr$uproc','nbr$uproc')
| 'nbr$uproc' = 'nbr$uproc' ),
inference(demodulation,[status(thm)],[d70,d55]) ).
cnf(d72,plain,
'nbr$uproc' = 'nbr$uproc',
inference(resolution,[status(thm)],[c88,d71]) ).
cnf(d73,plain,
( ~ setIn(X0,alive)
| ~ elem('m$uDown'(sK167),queue(host(X0)))
| norm != norm ),
inference(resolution,[status(thm)],[d72,d68]) ).
cnf(d74,plain,
( ~ setIn(X0,alive)
| ~ elem('m$uDown'(sK167),queue(host(X0))) ),
inference(equality_resolution,[status(thm)],[d73]) ).
cnf(d75,plain,
( elem('m$uDown'(sK167),queue(host(sK168)))
| 'm$uDown'(sK167) = 'm$uAck'(sK168,sK125) ),
inference(demodulation,[status(thm)],[d3,d35]) ).
cnf(d76,plain,
( ~ setIn(sK168,alive)
| 'm$uDown'(sK167) = 'm$uAck'(sK168,sK125) ),
inference(resolution,[status(thm)],[d75,d74]) ).
cnf(d77,plain,
'm$uDown'(sK167) = 'm$uAck'(sK168,sK125),
inference(resolution,[status(thm)],[c124,d76]) ).
cnf(d78,plain,
~ pidElem('m$uDown'(sK167)),
inference(superposition,[status(thm)],[d77,d2]) ).
cnf(d79,plain,
pidElem('m$uDown'(X0)),
inference(equality_resolution,[status(thm)],[c60]) ).
cnf(d80,plain,
$false,
inference(resolution,[status(thm)],[d79,d78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV462+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sat Sep 26 14:01:14 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 73.35/9.90 % SZS status Theorem for theBenchmark.p
% 73.35/9.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------