%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM571+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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 02:20:24 PM UTC 2026
% Result : Theorem 26.75s 4.35s
% Output : Proof 26.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 26 ( 6 unt; 0 def)
% Number of atoms : 153 ( 24 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 172 ( 45 ~; 40 |; 76 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 23 ( 0 sgn 19 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f80,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,W0))
& ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ( ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> aElementOf0(W1,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,W0)) ) ) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))
=> aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
<=> ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3623) ).
fof(f80_nnf,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ! [W1] :
( ( W1 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0))
| ~ aElement0(W1)
| aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) )
| ~ aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ! [W1] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) )
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [W0,W1] :
( ( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )
& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& ( W1 = szmzizndt0(sdtlpdtrp0(xN,W0))
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0))
| ~ aElement0(W1)
| aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& ( ( W1 != szmzizndt0(sdtlpdtrp0(xN,W0))
& aElementOf0(W1,sdtlpdtrp0(xN,W0))
& aElement0(W1) )
| ~ aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))
& ( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ( ~ aElementOf0(sk29(W0),szNzAzT0)
& aElementOf0(sk29(W0),sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) )
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk29])],[f80_nnf]) ).
cnf(c323,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
fof(f83,hypothesis,
( xi != sz00
=> ( isCountable0(sdtlpdtrp0(xN,xi))
& aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,xi))
& ? [W0] :
( szszuzczcdt0(W0) = xi
& aElementOf0(W0,szNzAzT0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3702_02) ).
fof(f83_nnf,plain,
( ( isCountable0(sdtlpdtrp0(xN,xi))
& aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aSet0(sdtlpdtrp0(xN,xi))
& ? [W0] :
( szszuzczcdt0(W0) = xi
& aElementOf0(W0,szNzAzT0) ) )
| xi = sz00 ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,xi))
& aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aSet0(sdtlpdtrp0(xN,xi))
& szszuzczcdt0(sk30) = xi
& aElementOf0(sk30,szNzAzT0) )
| xi = sz00 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk30])],[f83_nnf]) ).
cnf(c366,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| xi = sz00 ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
fof(f84,conjecture,
( isCountable0(sdtlpdtrp0(xN,xi))
& ( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f84_neg,negated_conjecture,
~ ( isCountable0(sdtlpdtrp0(xN,xi))
& ( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| ( ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xi))
=> aElementOf0(W0,szNzAzT0) )
& aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
inference(negated_conjecture,[status(cth)],[f84]) ).
fof(f84_nnf,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ( ? [W0] :
( ~ aElementOf0(W0,szNzAzT0)
& aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
| ~ aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
inference(nnf_transformation,[status(thm)],[f84_neg]) ).
fof(f84_sk,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ( ( ~ aElementOf0(sk31,szNzAzT0)
& aElementOf0(sk31,sdtlpdtrp0(xN,xi)) )
| ~ aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk31])],[f84_nnf]) ).
cnf(c370,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(p730,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| xi = sz00 ),
inference(resolution,[status(thm)],[c366,c370]) ).
cnf(c367,plain,
( isCountable0(sdtlpdtrp0(xN,xi))
| xi = sz00 ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(p731,plain,
( xi = sz00
| xi = sz00 ),
inference(resolution,[status(thm)],[p730,c367]) ).
cnf(p732,plain,
xi = sz00,
inference(factoring,[status(thm)],[p731]) ).
cnf(p739,plain,
( ~ isCountable0(sdtlpdtrp0(xN,sz00))
| ~ aSubsetOf0(sdtlpdtrp0(xN,sz00),szNzAzT0) ),
inference(demodulation,[status(thm)],[p732,c370]) ).
cnf(p742,plain,
( ~ isCountable0(xS)
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(superposition,[status(thm)],[c323,p739]) ).
fof(f74,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3435) ).
fof(f74_nnf,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
! [W0] :
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c170,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(p743,plain,
~ isCountable0(xS),
inference(resolution,[status(thm)],[p742,c170]) ).
cnf(c171,plain,
isCountable0(xS),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(p744,plain,
$false,
inference(resolution,[status(thm)],[p743,c171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM571+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.37 % Computer : n005.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.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Thu Sep 24 04:40:47 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.75/4.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.75/4.35 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------