%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM571+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 01:41:02 PM UTC 2026
% Result : Theorem 0.15s 0.49s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 43
% Syntax : Number of formulae : 171 ( 19 unt; 29 def)
% Number of atoms : 596 ( 69 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 671 ( 246 ~; 245 |; 125 &)
% ( 34 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 27 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 10 con; 0-2 aty)
% Number of variables : 147 ( 137 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [W0] :
( ( isCountable0(W0)
& aSet0(W0) )
=> ~ isFinite0(W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0] :
( ( isCountable0(W0)
& aSet0(W0) )
=> W0 != slcrc0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [W0,W1] :
( ( aSet0(W1)
& aSet0(W0) )
=> ( ( aSubsetOf0(W1,W0)
& aSubsetOf0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [W0,W1,W2] :
( ( aSet0(W2)
& aSet0(W1)
& aSet0(W0) )
=> ( ( aSubsetOf0(W1,W2)
& aSubsetOf0(W0,W1) )
=> aSubsetOf0(W0,W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,hypothesis,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,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') ).
fof(f82,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,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') ).
fof(f85,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') ).
fof(f86,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)],[f85]) ).
fof(f93,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f94,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f97,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f98,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f98]) ).
fof(f100,plain,
( ! [W0] :
( aElementOf0(sK0_skl(W0),W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f99]) ).
fof(f101,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f103,plain,
! [X0] :
( aElementOf0(sK0_skl(X0),X0)
| ~ aSet0(X0)
| X0 = slcrc0 ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f107,plain,
! [W0] :
( ~ isFinite0(W0)
| ~ isCountable0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f108,plain,
! [X0] :
( ~ isFinite0(X0)
| ~ isCountable0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [W0] :
( W0 != slcrc0
| ~ isCountable0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f110,plain,
! [X0] :
( X0 != slcrc0
| ~ isCountable0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f112,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f112]) ).
fof(f114,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f113]) ).
fof(f115,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f121,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f122,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [W0,W1] :
( W0 = W1
| ~ aSubsetOf0(W1,W0)
| ~ aSubsetOf0(W0,W1)
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f124,plain,
! [X0,X1] :
( X0 = X1
| ~ aSubsetOf0(X1,X0)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,plain,
! [W0,W1,W2] :
( aSubsetOf0(W0,W2)
| ~ aSubsetOf0(W1,W2)
| ~ aSubsetOf0(W0,W1)
| ~ aSet0(W2)
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f126,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f163,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f164,plain,
isCountable0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f345,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f346,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f347,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f349,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f350,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f346]) ).
fof(f381,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f383,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] :
( 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] :
( 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(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f384,definition,
! [W0] :
( sP4_prd(W0)
<=> ( ~ isCountable0(sdtlpdtrp0(xN,W0))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
& ( ? [W1] :
( ~ aElementOf0(W1,szNzAzT0)
& aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
| ~ aSet0(sdtlpdtrp0(xN,W0)) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f385,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] :
( 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] :
( sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(formula_renaming,[status(thm)],[f383,f384]) ).
fof(f386,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)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(NNF_transformation,[status(thm)],[f385]) ).
fof(f387,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] :
( ( 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)) )
| sP4_prd(W0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(miniscoping,[status(thm)],[f386]) ).
fof(f390,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f387]) ).
fof(f402,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f408,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(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f409,plain,
( ( isCountable0(sdtlpdtrp0(xN,xi))
& aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
& aSet0(sdtlpdtrp0(xN,xi))
& szszuzczcdt0(sK23_skl) = xi
& aElementOf0(sK23_skl,szNzAzT0) )
| xi = sz00 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W0,sK23_skl)],[f408]) ).
fof(f414,plain,
( aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
| xi = sz00 ),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f415,plain,
( isCountable0(sdtlpdtrp0(xN,xi))
| xi = sz00 ),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f416,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ( ? [W0] :
( ~ aElementOf0(W0,szNzAzT0)
& aElementOf0(W0,sdtlpdtrp0(xN,xi)) )
| ~ aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f417,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ( ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)
& ( ( ~ aElementOf0(sK24_skl,szNzAzT0)
& aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi)) )
| ~ aSet0(sdtlpdtrp0(xN,xi)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f416]) ).
fof(f420,plain,
( ~ isCountable0(sdtlpdtrp0(xN,xi))
| ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f417]) ).
fof(f496,definition,
( sQ0_spl
<=> xi = sz00 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( ~ sQ0_spl
| xi = sz00 ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f515,definition,
( sQ5_spl
<=> aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f517,plain,
( sQ5_spl
| ~ aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) ),
inference(component_clause,[status(thm)],[f515]) ).
fof(f518,plain,
( sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f414,f496,f515]) ).
fof(f519,definition,
( sQ6_spl
<=> isCountable0(sdtlpdtrp0(xN,xi)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f521,plain,
( sQ6_spl
| ~ isCountable0(sdtlpdtrp0(xN,xi)) ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f522,plain,
( sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f415,f496,f519]) ).
fof(f531,plain,
( ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f420,f515,f519]) ).
fof(f532,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f101]) ).
fof(f533,plain,
! [X0] : ~ aElementOf0(X0,slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f102]) ).
fof(f534,plain,
( ~ isCountable0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f110]) ).
fof(f585,plain,
! [X0] :
( aElementOf0(xi,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f116,f402]) ).
fof(f586,plain,
( ~ aSet0(szNzAzT0)
| aElementOf0(xi,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f585,f122]) ).
fof(f587,definition,
( sQ9_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f589,plain,
( sQ9_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f587]) ).
fof(f590,definition,
( sQ10_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f593,plain,
( sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f586,f587,f590]) ).
fof(f594,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f589,f163]) ).
fof(f595,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f594]) ).
fof(f596,plain,
! [X0,X1] :
( X1 = X0
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f124,f115]) ).
fof(f598,plain,
! [X0,X1,X2] :
( aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f126,f115]) ).
fof(f600,plain,
( aElement0(xi)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f94,f402]) ).
fof(f601,definition,
( sQ11_spl
<=> aElement0(xi) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( sQ11_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f600,f587,f601]) ).
fof(f608,plain,
( aElement0(xK)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f345,f94]) ).
fof(f609,plain,
! [X0] :
( aElementOf0(xK,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f345,f116]) ).
fof(f610,definition,
( sQ12_spl
<=> aElement0(xK) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( sQ12_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f608,f587,f610]) ).
fof(f614,plain,
! [X0] :
( aSubsetOf0(xS,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f349,f598]) ).
fof(f615,plain,
( xS = szNzAzT0
| ~ aSubsetOf0(szNzAzT0,xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f349,f596]) ).
fof(f616,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f349,f115]) ).
fof(f617,definition,
! [X0] :
( sQ13_spl
<=> ( aSubsetOf0(xS,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f618,plain,
! [X0] :
( ~ sQ13_spl
| aSubsetOf0(xS,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(component_clause,[status(thm)],[f617]) ).
fof(f620,plain,
( sQ13_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f614,f587,f617]) ).
fof(f621,definition,
( sQ14_spl
<=> aSubsetOf0(szNzAzT0,xS) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f624,definition,
( sQ15_spl
<=> xS = szNzAzT0 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( sQ15_spl
| ~ sQ14_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f615,f587,f621,f624]) ).
fof(f628,definition,
( sQ16_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f631,plain,
( sQ16_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f616,f587,f628]) ).
fof(f632,plain,
( aElement0(xk)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f381,f94]) ).
fof(f633,plain,
! [X0] :
( aElementOf0(xk,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f381,f116]) ).
fof(f634,definition,
( sQ17_spl
<=> aElement0(xk) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( sQ17_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f632,f587,f634]) ).
fof(f638,plain,
( ~ aSet0(slcrc0)
| slcrc0 = slcrc0 ),
inference(resolution,[status(thm)],[f103,f533]) ).
fof(f640,plain,
! [X0,X1] :
( aElementOf0(sK0_skl(X0),X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0)
| X0 = slcrc0 ),
inference(resolution,[status(thm)],[f103,f116]) ).
fof(f641,definition,
( sQ18_spl
<=> slcrc0 = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f644,definition,
( sQ19_spl
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f646,plain,
( sQ19_spl
| ~ aSet0(slcrc0) ),
inference(component_clause,[status(thm)],[f644]) ).
fof(f647,plain,
( ~ sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f638,f641,f644]) ).
fof(f649,plain,
! [X0,X1] :
( aElementOf0(sK0_skl(X0),X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| X0 = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f640,f115]) ).
fof(f650,plain,
( ~ isFinite0(xS)
| ~ isCountable0(xS) ),
inference(resolution,[status(thm)],[f108,f347]) ).
fof(f653,plain,
( ~ isFinite0(szNzAzT0)
| ~ isCountable0(szNzAzT0) ),
inference(resolution,[status(thm)],[f108,f163]) ).
fof(f654,definition,
( sQ20_spl
<=> isCountable0(xS) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f656,plain,
( sQ20_spl
| ~ isCountable0(xS) ),
inference(component_clause,[status(thm)],[f654]) ).
fof(f657,definition,
( sQ21_spl
<=> isFinite0(xS) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f660,plain,
( ~ sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f650,f654,f657]) ).
fof(f675,definition,
( sQ26_spl
<=> isCountable0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f677,plain,
( sQ26_spl
| ~ isCountable0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f675]) ).
fof(f678,definition,
( sQ27_spl
<=> isFinite0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f681,plain,
( ~ sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f653,f675,f678]) ).
fof(f682,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f677,f164]) ).
fof(f683,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f682]) ).
fof(f684,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f656,f350]) ).
fof(f685,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f684]) ).
fof(f686,plain,
~ isCountable0(slcrc0),
inference(forward_subsumption_resolution,[status(thm)],[f534,f532]) ).
fof(f687,plain,
( ~ aSet0(szNzAzT0)
| aElementOf0(xK,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f609,f122]) ).
fof(f688,definition,
( sQ28_spl
<=> aElementOf0(xK,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( sQ28_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f687,f587,f688]) ).
fof(f692,plain,
( ~ sQ13_spl
| ~ aSet0(szNzAzT0)
| aSubsetOf0(xS,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f618,f122]) ).
fof(f693,definition,
( sQ29_spl
<=> aSubsetOf0(xS,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f696,plain,
( ~ sQ13_spl
| sQ29_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f692,f587,f693,f617]) ).
fof(f697,plain,
( ~ aSet0(szNzAzT0)
| aElementOf0(xk,szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f633,f122]) ).
fof(f698,definition,
( sQ30_spl
<=> aElementOf0(xk,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( sQ30_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f697,f587,f698]) ).
fof(f702,plain,
! [X0] :
( ~ aSubsetOf0(X0,slcrc0)
| ~ aSet0(slcrc0)
| X0 = slcrc0 ),
inference(resolution,[status(thm)],[f649,f533]) ).
fof(f703,plain,
! [X0,X1] :
( aElement0(sK0_skl(X0))
| ~ aSet0(X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| X0 = slcrc0 ),
inference(resolution,[status(thm)],[f649,f94]) ).
fof(f704,plain,
! [X0,X1,X2] :
( aElementOf0(sK0_skl(X0),X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| X0 = slcrc0 ),
inference(resolution,[status(thm)],[f649,f116]) ).
fof(f705,definition,
! [X0] :
( sQ31_spl
<=> ( ~ aSubsetOf0(X0,slcrc0)
| X0 = slcrc0 ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f708,plain,
( ~ sQ19_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f702,f705,f644]) ).
fof(f709,plain,
! [X0,X1] :
( aElement0(sK0_skl(X0))
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X1)
| X0 = slcrc0 ),
inference(duplicate_literals_removal,[status(thm)],[f703]) ).
fof(f710,plain,
! [X0,X1,X2] :
( aElementOf0(sK0_skl(X0),X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2)
| ~ aSubsetOf0(X0,X1)
| X0 = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f704,f115]) ).
fof(f711,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f646,f532]) ).
fof(f712,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f711]) ).
fof(f715,plain,
( aElement0(sK0_skl(xS))
| ~ aSet0(szNzAzT0)
| xS = slcrc0 ),
inference(resolution,[status(thm)],[f709,f349]) ).
fof(f717,definition,
( sQ32_spl
<=> xS = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f718,plain,
( ~ sQ32_spl
| xS = slcrc0 ),
inference(component_clause,[status(thm)],[f717]) ).
fof(f720,definition,
( sQ33_spl
<=> aElement0(sK0_skl(xS)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f723,plain,
( sQ33_spl
| ~ sQ9_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f715,f717,f587,f720]) ).
fof(f728,plain,
( ~ sQ32_spl
| ~ isCountable0(xS) ),
inference(backward_demodulation,[status(thm)],[f718,f686]) ).
fof(f735,plain,
( ~ sQ32_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f728,f654,f717]) ).
fof(f746,plain,
! [X0,X1,X2] :
( aElement0(sK0_skl(X0))
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2)
| ~ aSubsetOf0(X0,X1)
| X0 = slcrc0 ),
inference(resolution,[status(thm)],[f710,f94]) ).
fof(f748,plain,
! [X0,X1,X2] :
( aElement0(sK0_skl(X0))
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2)
| ~ aSubsetOf0(X0,X1)
| X0 = slcrc0 ),
inference(duplicate_literals_removal,[status(thm)],[f746]) ).
fof(f750,plain,
! [X0] :
( aElement0(sK0_skl(X0))
| ~ aSet0(szNzAzT0)
| ~ aSubsetOf0(X0,xS)
| X0 = slcrc0 ),
inference(resolution,[status(thm)],[f748,f349]) ).
fof(f752,definition,
! [X0] :
( sQ34_spl
<=> ( aElement0(sK0_skl(X0))
| ~ aSubsetOf0(X0,xS)
| X0 = slcrc0 ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f755,plain,
( ~ sQ9_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f750,f752,f587]) ).
fof(f759,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,slcrc0)
| ~ aSet0(slcrc0)
| ~ aSubsetOf0(X0,X1)
| X0 = slcrc0 ),
inference(resolution,[status(thm)],[f533,f710]) ).
fof(f761,definition,
! [X0,X1] :
( sQ35_spl
<=> ( ~ aSubsetOf0(X1,slcrc0)
| ~ aSubsetOf0(X0,X1)
| X0 = slcrc0 ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f764,plain,
( ~ sQ19_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f759,f761,f644]) ).
fof(f772,plain,
( ~ sQ0_spl
| sdtlpdtrp0(xN,xi) = xS ),
inference(forward_demodulation,[status(thm)],[f497,f390]) ).
fof(f773,plain,
( sQ6_spl
| ~ sQ0_spl
| ~ isCountable0(xS) ),
inference(forward_demodulation,[status(thm)],[f772,f521]) ).
fof(f774,plain,
( sQ6_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f773,f350]) ).
fof(f775,plain,
( sQ6_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f774]) ).
fof(f780,plain,
( sQ5_spl
| ~ sQ0_spl
| ~ aSubsetOf0(xS,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f772,f517]) ).
fof(f781,plain,
( sQ5_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f780,f349]) ).
fof(f782,plain,
( sQ5_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f781]) ).
fof(f783,plain,
$false,
inference(sat_refutation,[status(thm)],[f518,f522,f531,f593,f595,f604,f613,f620,f627,f631,f637,f647,f660,f681,f683,f685,f691,f696,f701,f708,f712,f723,f735,f755,f764,f775,f782]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM571+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n020.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 02:41:49 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.46 % Drodi V4.1.1
% 0.15/0.49 % Refutation found
% 0.15/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.53 % Elapsed time: 0.085216 seconds
% 0.15/0.53 % CPU time: 0.273267 seconds
% 0.15/0.53 % Total memory used: 65.093 MB
% 0.15/0.53 % Net memory used: 64.932 MB
%------------------------------------------------------------------------------