%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV465+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Sun Sep 27 09:02:28 AM UTC 2026
% Result : Theorem 30.82s 9.76s
% Output : CNFRefutation 30.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 5
% Syntax : Number of formulae : 52 ( 24 unt; 0 def)
% Number of atoms : 351 ( 164 equ)
% Maximal formula atoms : 88 ( 6 avg)
% Number of connectives : 482 ( 183 ~; 129 |; 124 &)
% ( 2 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 18 con; 0-2 aty)
% Number of variables : 150 ( 6 sgn 101 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_13,axiom,
! [X0,X1,X2] : 'm$uAck'(X0,X1) != 'm$uNotNorm'(X2) ).
fof(axiom_19,axiom,
! [X0,X1] : 'm$uDown'(X0) != 'm$uNotNorm'(X1) ).
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(conj,conjecture,
! [X0,X1,X2] :
( ( queue(host(X2)) = cons('m$uNormQ'(X1),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(X2,alive)
=> ( index(status,host(X2)) != norm
=> ! [X3,X4,X8,X9] :
( host(X1) = host(X9)
=> ( host(X2) = host(X9)
=> ( ( host(X8) = s(index(pendack,host(X9)))
& host(X4) = index(pendack,host(X9))
& index(status,host(X9)) = 'elec$u2'
& leq('nbr$uproc',s(index(pendack,host(X9))))
& elem('m$uAck'(X9,X4),snoc(X0,'m$uNotNorm'(X1)))
& elem('m$uDown'(X8),snoc(X0,'m$uNotNorm'(X1)))
& 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(X2)) = cons('m$uNormQ'(X1),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(X2,alive)
=> ( index(status,host(X2)) != norm
=> ! [X3,X4,X8,X9] :
( host(X1) = host(X9)
=> ( host(X2) = host(X9)
=> ( ( host(X8) = s(index(pendack,host(X9)))
& host(X4) = index(pendack,host(X9))
& index(status,host(X9)) = 'elec$u2'
& leq('nbr$uproc',s(index(pendack,host(X9))))
& elem('m$uAck'(X9,X4),snoc(X0,'m$uNotNorm'(X1)))
& elem('m$uDown'(X8),snoc(X0,'m$uNotNorm'(X1)))
& setIn(X9,alive) )
=> ~ ( index(status,host(X3)) = norm
& index(ldr,host(X3)) = host(X3)
& setIn(X3,alive) ) ) ) ) ) ) ),
inference(negate_conjecture,[status(cth)],[conj]) ).
cnf(c14,plain,
'm$uAck'(X0,X1) != 'm$uNotNorm'(X2),
inference(clausification,[status(esa)],[axiom_13]) ).
cnf(c20,plain,
'm$uDown'(X0) != 'm$uNotNorm'(X1),
inference(clausification,[status(esa)],[axiom_19]) ).
cnf(c54,plain,
( ~ elem(X0,X2)
| 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(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(sK126)) = cons('m$uNormQ'(sK125),sK124),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c123,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,
elem('m$uDown'(sK167),snoc(sK124,'m$uNotNorm'(sK125))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c126,plain,
elem('m$uAck'(sK168,sK166),snoc(sK124,'m$uNotNorm'(sK125))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c127,plain,
leq('nbr$uproc',s(index(pendack,host(sK168)))),
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,
( elem('m$uAck'(sK168,sK166),sK124)
| 'm$uAck'(sK168,sK166) = 'm$uNotNorm'(sK125) ),
inference(resolution,[status(thm)],[c55,c126]) ).
cnf(d1,plain,
elem('m$uAck'(sK168,sK166),sK124),
inference(resolution,[status(thm)],[c14,d0]) ).
cnf(d2,plain,
queue(host(sK168)) = cons('m$uNormQ'(sK125),sK124),
inference(demodulation,[status(thm)],[c119,c123]) ).
cnf(d3,plain,
( ~ elem(X0,sK124)
| elem(X0,queue(host(sK168))) ),
inference(superposition,[status(thm)],[d2,c54]) ).
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)],[c127,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$uDown'(sK167),queue(host(sK168)))
| ~ elem('m$uAck'(sK168,sK166),sK124) ),
inference(resolution,[status(thm)],[d3,d22]) ).
cnf(d24,plain,
( ~ elem('m$uDown'(sK167),sK124)
| ~ elem('m$uAck'(sK168,sK166),sK124) ),
inference(resolution,[status(thm)],[d23,d3]) ).
cnf(d25,plain,
( elem('m$uDown'(sK167),sK124)
| 'm$uDown'(sK167) = 'm$uNotNorm'(sK125) ),
inference(resolution,[status(thm)],[c55,c125]) ).
cnf(d26,plain,
elem('m$uDown'(sK167),sK124),
inference(resolution,[status(thm)],[c20,d25]) ).
cnf(d27,plain,
~ elem('m$uAck'(sK168,sK166),sK124),
inference(resolution,[status(thm)],[d26,d24]) ).
cnf(d28,plain,
$false,
inference(resolution,[status(thm)],[d27,d1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV465+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n008.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 13:55:46 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.82/9.76 % SZS status Theorem for theBenchmark.p
% 30.82/9.76 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------