%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV457+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 33.02s 4.66s
% Output : CNFRefutation 33.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 7
% Syntax : Number of formulae : 71 ( 27 unt; 0 def)
% Number of atoms : 349 ( 159 equ)
% Maximal formula atoms : 72 ( 4 avg)
% Number of connectives : 464 ( 186 ~; 134 |; 97 &)
% ( 3 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 17 con; 0-2 aty)
% Number of variables : 153 ( 21 sgn 97 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_04,axiom,
! [X0] : leq(host(X0),'nbr$uproc') ).
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_61,axiom,
! [X0,X1] :
( ( leq(X1,X0)
& leq(X0,X1) )
<=> X0 = X1 ) ).
fof(conj,conjecture,
! [X0,X1,X2] :
( ( queue(host(X1)) = cons('m$uHalt'(X2),X0)
& ! [X3,X4,X5] :
( ( host(X4) = index(pendack,host(X5))
& index(status,host(X5)) = 'elec$u2'
& leq('nbr$uproc',index(pendack,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,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] :
( ( host(X4) = host(X3)
& elem('m$uAck'(X5,X3),queue(host(X5)))
& setIn(X5,alive)
& setIn(X4,alive) )
=> ~ setIn(host(X5),index(down,host(X4))) )
& ! [X3,X4,X5] :
( ( host(X5) = host(X3)
& elem('m$uAck'(X5,X4),queue(host(X5)))
& elem('m$uDown'(X3),queue(host(X4))) )
=> ~ setIn(X5,alive) )
& ! [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] :
( ( index(status,host(X4)) = 'elec$u1'
& setIn(X4,alive) )
=> ~ elem('m$uAck'(X3,X4),queue(host(X3))) )
& ! [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] :
( ( host(X4) = host(X3)
& leq(X4,X3)
& ~ setIn(X3,alive) )
=> ~ setIn(X4,alive) )
& ! [X3,X4,X5] :
( elem('m$uAck'(X5,X3),queue(host(X4)))
=> ~ leq(host(X3),host(X5)) )
& ! [X3,X4] :
( elem('m$uLdr'(X4),queue(host(X3)))
=> ~ leq(host(X3),host(X4)) )
& ! [X3,X4] :
( elem('m$uDown'(X4),queue(host(X3)))
=> ~ setIn(X4,alive) )
& ! [X3,X4] :
( elem('m$uAck'(X4,X3),queue(host(X4)))
=> setIn(X4,pids) ) )
=> ( setIn(X1,alive)
=> ! [X3] :
( host(X1) != host(X3)
=> ! [X4,X6] :
( host(X2) = host(X6)
=> ( host(X1) != host(X6)
=> ( ( host(X4) = index(pendack,host(X6))
& index(status,host(X6)) = 'elec$u2'
& elem('m$uAck'(X6,X4),snoc(queue(host(X6)),'m$uAck'(X2,X1)))
& leq('nbr$uproc',index(pendack,host(X6)))
& setIn(X6,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,X5] :
( ( host(X4) = index(pendack,host(X5))
& index(status,host(X5)) = 'elec$u2'
& leq('nbr$uproc',index(pendack,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,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] :
( ( host(X4) = host(X3)
& elem('m$uAck'(X5,X3),queue(host(X5)))
& setIn(X5,alive)
& setIn(X4,alive) )
=> ~ setIn(host(X5),index(down,host(X4))) )
& ! [X3,X4,X5] :
( ( host(X5) = host(X3)
& elem('m$uAck'(X5,X4),queue(host(X5)))
& elem('m$uDown'(X3),queue(host(X4))) )
=> ~ setIn(X5,alive) )
& ! [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] :
( ( index(status,host(X4)) = 'elec$u1'
& setIn(X4,alive) )
=> ~ elem('m$uAck'(X3,X4),queue(host(X3))) )
& ! [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] :
( ( host(X4) = host(X3)
& leq(X4,X3)
& ~ setIn(X3,alive) )
=> ~ setIn(X4,alive) )
& ! [X3,X4,X5] :
( elem('m$uAck'(X5,X3),queue(host(X4)))
=> ~ leq(host(X3),host(X5)) )
& ! [X3,X4] :
( elem('m$uLdr'(X4),queue(host(X3)))
=> ~ leq(host(X3),host(X4)) )
& ! [X3,X4] :
( elem('m$uDown'(X4),queue(host(X3)))
=> ~ setIn(X4,alive) )
& ! [X3,X4] :
( elem('m$uAck'(X4,X3),queue(host(X4)))
=> setIn(X4,pids) ) )
=> ( setIn(X1,alive)
=> ! [X3] :
( host(X1) != host(X3)
=> ! [X4,X6] :
( host(X2) = host(X6)
=> ( host(X1) != host(X6)
=> ( ( host(X4) = index(pendack,host(X6))
& index(status,host(X6)) = 'elec$u2'
& elem('m$uAck'(X6,X4),snoc(queue(host(X6)),'m$uAck'(X2,X1)))
& leq('nbr$uproc',index(pendack,host(X6)))
& setIn(X6,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(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(c90,plain,
( X0 = X1
| ~ leq(X1,X0)
| ~ leq(X0,X1) ),
inference(clausification,[status(esa)],[axiom_61]) ).
cnf(c114,plain,
( leq(index(pendack,host(X0)),host(X2))
| index(ldr,host(X2)) != host(X2)
| ~ setIn(X2,alive)
| ~ setIn(X0,alive)
| index(status,host(X2)) != norm
| ~ elem('m$uHalt'(X0),queue(host(X1)))
| index(status,host(X0)) != 'elec$u2' ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c115,plain,
( ~ setIn(X2,alive)
| index(status,host(X2)) != 'elec$u2'
| index(ldr,host(X0)) != host(X0)
| ~ elem('m$uAck'(X2,X1),queue(host(X2)))
| index(status,host(X0)) != norm
| ~ leq('nbr$uproc',index(pendack,host(X2)))
| host(X1) != index(pendack,host(X2))
| ~ setIn(X0,alive) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c116,plain,
queue(host(sK125)) = cons('m$uHalt'(sK126),sK124),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c118,plain,
host(sK125) != host(sK161),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c119,plain,
host(sK126) = host(sK163),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c121,plain,
setIn(sK163,alive),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c122,plain,
leq('nbr$uproc',index(pendack,host(sK163))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c123,plain,
elem('m$uAck'(sK163,sK162),snoc(queue(host(sK163)),'m$uAck'(sK126,sK125))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c124,plain,
index(status,host(sK163)) = 'elec$u2',
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c125,plain,
host(sK162) = index(pendack,host(sK163)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c126,plain,
setIn(sK161,alive),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c127,plain,
index(ldr,host(sK161)) = host(sK161),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c128,plain,
index(status,host(sK161)) = norm,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( elem('m$uAck'(sK163,sK162),queue(host(sK163)))
| 'm$uAck'(sK163,sK162) = 'm$uAck'(sK126,sK125) ),
inference(resolution,[status(thm)],[c55,c123]) ).
cnf(d1,plain,
( ~ leq('nbr$uproc',index(pendack,host(X1)))
| ~ setIn(X1,alive)
| ~ setIn(sK161,alive)
| ~ elem('m$uAck'(X1,X0),queue(host(X1)))
| index(status,host(X1)) != 'elec$u2'
| index(status,host(sK161)) != norm
| host(X0) != index(pendack,host(X1))
| host(sK161) != host(sK161) ),
inference(superposition,[status(thm)],[c127,c115]) ).
cnf(d2,plain,
( ~ leq('nbr$uproc',index(pendack,host(X1)))
| ~ setIn(sK161,alive)
| ~ setIn(X1,alive)
| ~ elem('m$uAck'(X1,X0),queue(host(X1)))
| norm != norm
| index(status,host(X1)) != 'elec$u2'
| host(sK161) != host(sK161)
| host(X0) != index(pendack,host(X1)) ),
inference(demodulation,[status(thm)],[d1,c128]) ).
cnf(d3,plain,
( ~ leq('nbr$uproc',index(pendack,host(X1)))
| ~ setIn(X1,alive)
| ~ elem('m$uAck'(X1,X0),queue(host(X1)))
| norm != norm
| index(status,host(X1)) != 'elec$u2'
| host(sK161) != host(sK161)
| host(X0) != index(pendack,host(X1)) ),
inference(resolution,[status(thm)],[c126,d2]) ).
cnf(d4,plain,
( ~ leq('nbr$uproc',index(pendack,host(sK163)))
| ~ setIn(sK163,alive)
| ~ elem('m$uAck'(sK163,X0),queue(host(sK163)))
| index(status,host(sK163)) != 'elec$u2'
| norm != norm
| host(sK161) != host(sK161)
| host(X0) != host(sK162) ),
inference(superposition,[status(thm)],[c125,d3]) ).
cnf(d5,plain,
( ~ leq('nbr$uproc',index(pendack,host(sK163)))
| ~ setIn(sK163,alive)
| ~ elem('m$uAck'(sK163,X0),queue(host(sK163)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK161) != host(sK161)
| host(X0) != host(sK162) ),
inference(demodulation,[status(thm)],[d4,c124]) ).
cnf(d6,plain,
( ~ leq('nbr$uproc',host(sK162))
| ~ setIn(sK163,alive)
| ~ elem('m$uAck'(sK163,X0),queue(host(sK163)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK161) != host(sK161)
| host(X0) != host(sK162) ),
inference(demodulation,[status(thm)],[d5,c125]) ).
cnf(d7,plain,
( ~ leq('nbr$uproc',host(sK162))
| ~ elem('m$uAck'(sK163,X0),queue(host(sK163)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK161) != host(sK161)
| host(X0) != host(sK162) ),
inference(resolution,[status(thm)],[c121,d6]) ).
cnf(d8,plain,
leq('nbr$uproc',host(sK162)),
inference(demodulation,[status(thm)],[c122,c125]) ).
cnf(d9,plain,
( ~ elem('m$uAck'(sK163,X0),queue(host(sK163)))
| norm != norm
| 'elec$u2' != 'elec$u2'
| host(sK161) != host(sK161)
| host(X0) != host(sK162) ),
inference(resolution,[status(thm)],[d8,d7]) ).
cnf(d10,plain,
( ~ elem('m$uAck'(sK163,X0),queue(host(sK163)))
| norm != norm
| 'elec$u2' != 'elec$u2'
| host(X0) != host(sK162) ),
inference(equality_resolution,[status(thm)],[d9]) ).
cnf(d11,plain,
( ~ elem('m$uAck'(sK163,sK162),queue(host(sK163)))
| norm != norm
| 'elec$u2' != 'elec$u2' ),
inference(equality_resolution,[status(thm)],[d10]) ).
cnf(d12,plain,
( ~ elem('m$uAck'(sK163,sK162),queue(host(sK163)))
| 'elec$u2' != 'elec$u2' ),
inference(equality_resolution,[status(thm)],[d11]) ).
cnf(d13,plain,
~ elem('m$uAck'(sK163,sK162),queue(host(sK163))),
inference(equality_resolution,[status(thm)],[d12]) ).
cnf(d14,plain,
'm$uAck'(sK163,sK162) = 'm$uAck'(sK126,sK125),
inference(resolution,[status(thm)],[d13,d0]) ).
cnf(d15,plain,
( sK125 = X1
| 'm$uAck'(sK163,sK162) != 'm$uAck'(X0,X1) ),
inference(superposition,[status(thm)],[d14,c38]) ).
cnf(d16,plain,
sK125 = sK162,
inference(equality_resolution,[status(thm)],[d15]) ).
cnf(d17,plain,
leq('nbr$uproc',host(sK125)),
inference(demodulation,[status(thm)],[d8,d16]) ).
cnf(d18,plain,
( ~ leq(host(sK125),'nbr$uproc')
| 'nbr$uproc' = host(sK125) ),
inference(resolution,[status(thm)],[c90,d17]) ).
cnf(d19,plain,
'nbr$uproc' = host(sK125),
inference(resolution,[status(thm)],[c5,d18]) ).
cnf(d20,plain,
( X0 = sK126
| 'm$uAck'(X0,X1) != 'm$uAck'(sK163,sK162) ),
inference(superposition,[status(thm)],[d14,c37]) ).
cnf(d21,plain,
( 'm$uAck'(X0,X1) != 'm$uAck'(sK163,sK125)
| X0 = sK126 ),
inference(demodulation,[status(thm)],[d20,d16]) ).
cnf(d22,plain,
sK163 = sK126,
inference(equality_resolution,[status(thm)],[d21]) ).
cnf(d23,plain,
( leq(index(pendack,host(X0)),host(sK161))
| ~ setIn(X0,alive)
| ~ setIn(sK161,alive)
| ~ elem('m$uHalt'(X0),queue(host(X1)))
| index(status,host(X0)) != 'elec$u2'
| index(status,host(sK161)) != norm
| host(sK161) != host(sK161) ),
inference(superposition,[status(thm)],[c127,c114]) ).
cnf(d24,plain,
( leq(index(pendack,host(X0)),host(sK161))
| ~ setIn(sK161,alive)
| ~ setIn(X0,alive)
| ~ elem('m$uHalt'(X0),queue(host(X1)))
| norm != norm
| index(status,host(X0)) != 'elec$u2'
| host(sK161) != host(sK161) ),
inference(demodulation,[status(thm)],[d23,c128]) ).
cnf(d25,plain,
( leq(index(pendack,host(X0)),host(sK161))
| ~ setIn(X0,alive)
| ~ elem('m$uHalt'(X0),queue(host(X1)))
| norm != norm
| index(status,host(X0)) != 'elec$u2'
| host(sK161) != host(sK161) ),
inference(resolution,[status(thm)],[c126,d24]) ).
cnf(d26,plain,
( leq(index(pendack,host(sK126)),host(sK161))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| norm != norm
| host(sK161) != host(sK161)
| index(status,host(sK163)) != 'elec$u2' ),
inference(superposition,[status(thm)],[c119,d25]) ).
cnf(d27,plain,
( leq(index(pendack,host(sK126)),host(sK161))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK161) != host(sK161) ),
inference(demodulation,[status(thm)],[d26,c124]) ).
cnf(d28,plain,
( leq(index(pendack,host(sK163)),host(sK161))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK161) != host(sK161) ),
inference(demodulation,[status(thm)],[d27,c119]) ).
cnf(d29,plain,
( leq(host(sK162),host(sK161))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm
| host(sK161) != host(sK161) ),
inference(demodulation,[status(thm)],[d28,c125]) ).
cnf(d30,plain,
( leq(host(sK162),host(sK161))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2'
| norm != norm ),
inference(equality_resolution,[status(thm)],[d29]) ).
cnf(d31,plain,
( leq(host(sK162),host(sK161))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0)))
| 'elec$u2' != 'elec$u2' ),
inference(equality_resolution,[status(thm)],[d30]) ).
cnf(d32,plain,
( leq(host(sK162),host(sK161))
| ~ setIn(sK126,alive)
| ~ elem('m$uHalt'(sK126),queue(host(X0))) ),
inference(equality_resolution,[status(thm)],[d31]) ).
cnf(d33,plain,
elem(X0,cons(X0,X1)),
inference(equality_resolution,[status(thm)],[c53]) ).
cnf(d34,plain,
elem('m$uHalt'(sK126),queue(host(sK125))),
inference(superposition,[status(thm)],[c116,d33]) ).
cnf(d35,plain,
( leq(host(sK162),host(sK161))
| ~ setIn(sK126,alive) ),
inference(resolution,[status(thm)],[d34,d32]) ).
cnf(d36,plain,
( leq(host(sK125),host(sK161))
| ~ setIn(sK126,alive) ),
inference(demodulation,[status(thm)],[d35,d16]) ).
cnf(d37,plain,
( leq(host(sK125),host(sK161))
| ~ setIn(sK163,alive) ),
inference(demodulation,[status(thm)],[d36,d22]) ).
cnf(d38,plain,
leq(host(sK125),host(sK161)),
inference(resolution,[status(thm)],[c121,d37]) ).
cnf(d39,plain,
leq('nbr$uproc',host(sK161)),
inference(demodulation,[status(thm)],[d38,d19]) ).
cnf(d40,plain,
( ~ leq(host(sK161),'nbr$uproc')
| 'nbr$uproc' = host(sK161) ),
inference(resolution,[status(thm)],[d39,c90]) ).
cnf(d41,plain,
'nbr$uproc' = host(sK161),
inference(resolution,[status(thm)],[c5,d40]) ).
cnf(d42,plain,
'nbr$uproc' != host(sK161),
inference(demodulation,[status(thm)],[c118,d19]) ).
cnf(d43,plain,
$false,
inference(resolution,[status(thm)],[d42,d41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV457+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 14:00:28 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.02/4.66 % SZS status Theorem for theBenchmark.p
% 33.02/4.66 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------