%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM629+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:15 PM UTC 2026
% Result : Theorem 34.08s 9.99s
% Output : CNFRefutation 34.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 19
% Syntax : Number of formulae : 104 ( 18 unt; 6 def)
% Number of atoms : 457 ( 81 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 594 ( 241 ~; 226 |; 95 &)
% ( 17 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 13 con; 0-3 aty)
% Number of variables : 172 ( 161 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,definition,
! [W0] :
( W0 = slcrc0
<=> ( ~ ? [W1] : aElementOf0(W1,W0)
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [W0] :
( ( isCountable0(W0)
& aSet0(W0) )
=> W0 != slcrc0 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f16,definition,
! [W0,W1] :
( ( aElement0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,definition,
! [W0] :
( ( W0 != slcrc0
& aSubsetOf0(W0,szNzAzT0) )
=> ! [W1] :
( W1 = szmzizndt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,W0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,definition,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aSet0(W0) )
=> ! [W2] :
( W2 = slbdtsldtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
( szszuzczcdt0(xk) = xK
& aElementOf0(xk,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )
=> ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
sbrdtbr0(xP) = xk,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,conjecture,
aElementOf0(xP,slbdtsldtrb0(xD,xk)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,negated_conjecture,
~ aElementOf0(xP,slbdtsldtrb0(xD,xk)),
inference(negated_conjecture,[status(cth)],[f115]) ).
fof(f123,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f124,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f127,plain,
! [W0] :
( W0 = slcrc0
<=> ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f128,plain,
! [W0] :
( ( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
( ! [W0] :
( ? [W1] : aElementOf0(W1,W0)
| ~ aSet0(W0)
| W0 = slcrc0 )
& ! [W0] :
( ( ! [W1] : ~ aElementOf0(W1,W0)
& aSet0(W0) )
| W0 != slcrc0 ) ),
inference(miniscoping,[status(thm)],[f128]) ).
fof(f130,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))],[f129]) ).
fof(f131,plain,
! [X0] :
( aSet0(X0)
| X0 != slcrc0 ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f139,plain,
! [W0] :
( W0 != slcrc0
| ~ isCountable0(W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f140,plain,
! [X0] :
( X0 != slcrc0
| ~ isCountable0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,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(f142,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)],[f141]) ).
fof(f143,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)],[f142]) ).
fof(f144,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))],[f143]) ).
fof(f145,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f151,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f152,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,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(f156,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f170,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f171,definition,
! [W0,W1,W3] :
( sP0_prd(W3,W1,W0)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f172,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtmndt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> sP0_prd(W3,W1,W0) )
& aSet0(W2) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(formula_renaming,[status(thm)],[f170,f171]) ).
fof(f173,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ~ sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ( ( ! [W3] :
( ( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ~ sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f175,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( sP0_prd(sK3_skl(W2,W1,W0),W1,W0)
| aElementOf0(sK3_skl(W2,W1,W0),W2) )
& ( ~ sP0_prd(sK3_skl(W2,W1,W0),W1,W0)
| ~ aElementOf0(sK3_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtmndt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ sP0_prd(W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( sP0_prd(W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtmndt0(W0,W1) ) )
| ~ aElement0(W1)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f174]) ).
fof(f176,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f193,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f251,plain,
! [W0] :
( ! [W1] :
( W1 = szmzizndt0(W0)
<=> ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f252,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ sdtlseqdt0(W1,W2)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzizndt0(W0) )
& ( ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzizndt0(W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(NNF_transformation,[status(thm)],[f251]) ).
fof(f253,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ sdtlseqdt0(W1,W2)
& aElementOf0(W2,W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzizndt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzizndt0(W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(miniscoping,[status(thm)],[f252]) ).
fof(f254,plain,
! [W0] :
( ( ! [W1] :
( ( ~ sdtlseqdt0(W1,sK6_skl(W1,W0))
& aElementOf0(sK6_skl(W1,W0),W0) )
| ~ aElementOf0(W1,W0)
| W1 = szmzizndt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlseqdt0(W1,W2)
| ~ aElementOf0(W2,W0) )
& aElementOf0(W1,W0) )
| W1 != szmzizndt0(W0) ) )
| W0 = slcrc0
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W2,sK6_skl(W1,W0))],[f253]) ).
fof(f255,plain,
! [X0,X1] :
( aElementOf0(X1,X0)
| X1 != szmzizndt0(X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f298,plain,
! [W0,W1] :
( ! [W2] :
( W2 = slbdtsldtrb0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) ) )
& aSet0(W2) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f299,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ( ( ! [W3] :
( ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f298]) ).
fof(f300,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f299]) ).
fof(f301,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( ( sbrdtbr0(sK10_skl(W2,W1,W0)) = W1
& aSubsetOf0(sK10_skl(W2,W1,W0),W0) )
| aElementOf0(sK10_skl(W2,W1,W0),W2) )
& ( sbrdtbr0(sK10_skl(W2,W1,W0)) != W1
| ~ aSubsetOf0(sK10_skl(W2,W1,W0),W0)
| ~ aElementOf0(sK10_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = slbdtsldtrb0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( sbrdtbr0(W3) != W1
| ~ aSubsetOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sbrdtbr0(W3) = W1
& aSubsetOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != slbdtsldtrb0(W0,W1) ) )
| ~ aElementOf0(W1,szNzAzT0)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f300]) ).
fof(f305,plain,
! [X0,X1,X2,X3] :
( sbrdtbr0(X3) != X1
| ~ aSubsetOf0(X3,X0)
| aElementOf0(X3,X2)
| X2 != slbdtsldtrb0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f389,plain,
aElementOf0(xk,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f391,plain,
( ! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))
& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )
| ~ isCountable0(sdtlpdtrp0(xN,W0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) )
& sdtlpdtrp0(xN,sz00) = xS
& szDzozmdt0(xN) = szNzAzT0
& aFunction0(xN) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f395,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f397,plain,
! [W0] :
( ( isCountable0(sdtlpdtrp0(xN,W0))
& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f398,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f399,plain,
! [X0] :
( isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f459,plain,
sbrdtbr0(xP) = xk,
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f462,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f465,plain,
aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f466,plain,
xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f467,plain,
~ aElementOf0(xP,slbdtsldtrb0(xD,xk)),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f474,plain,
aSet0(slcrc0),
inference(destructive_equality_resolution,[status(thm)],[f131]) ).
fof(f476,plain,
( ~ isCountable0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(destructive_equality_resolution,[status(thm)],[f140]) ).
fof(f483,plain,
! [X0,X1] :
( aSet0(sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f176]) ).
fof(f487,plain,
! [X0] :
( aElementOf0(szmzizndt0(X0),X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f255]) ).
fof(f500,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,X0)
| aElementOf0(X1,slbdtsldtrb0(X0,sbrdtbr0(X1)))
| ~ aElementOf0(sbrdtbr0(X1),szNzAzT0)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f305]) ).
fof(f571,plain,
~ isCountable0(slcrc0),
inference(forward_subsumption_resolution,[status(thm)],[f476,f474]) ).
fof(f778,plain,
! [X0,X1,X2] :
( aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f156,f145]) ).
fof(f1265,plain,
( aSet0(xD)
| ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| ~ aSet0(sdtlpdtrp0(xN,xn)) ),
inference(paramodulation,[status(thm)],[f466,f483]) ).
fof(f2671,plain,
! [X0] :
( aElement0(szmzizndt0(X0))
| ~ aSet0(X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f487,f124]) ).
fof(f2692,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aSet0(szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f398,f145]) ).
fof(f2696,plain,
! [X0] :
( aSet0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2692,f193]) ).
fof(f4194,plain,
! [X0] :
( ~ aSubsetOf0(xP,X0)
| aElementOf0(xP,slbdtsldtrb0(X0,xk))
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| ~ aSet0(X0) ),
inference(paramodulation,[status(thm)],[f459,f500]) ).
fof(f4200,plain,
! [X0] :
( ~ aSubsetOf0(xP,X0)
| aElementOf0(xP,slbdtsldtrb0(X0,xk))
| ~ aElementOf0(xk,szNzAzT0)
| ~ aSet0(X0) ),
inference(forward_demodulation,[status(thm)],[f459,f4194]) ).
fof(f4201,plain,
! [X0] :
( ~ aSubsetOf0(xP,X0)
| aElementOf0(xP,slbdtsldtrb0(X0,xk))
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4200,f389]) ).
fof(f4946,plain,
( ~ aSubsetOf0(xP,xD)
| ~ aSet0(xD) ),
inference(resolution,[status(thm)],[f4201,f467]) ).
fof(f4951,plain,
! [X0] :
( ~ aSubsetOf0(X0,xD)
| ~ aSubsetOf0(xP,X0)
| ~ aSet0(xD)
| ~ aSet0(X0)
| ~ aSet0(xD) ),
inference(resolution,[status(thm)],[f4946,f778]) ).
fof(f4952,plain,
! [X0] :
( ~ aSubsetOf0(X0,xD)
| ~ aSubsetOf0(xP,X0)
| ~ aSet0(X0)
| ~ aSet0(xD) ),
inference(duplicate_literals_removal,[status(thm)],[f4951]) ).
fof(f4953,plain,
! [X0] :
( ~ aSubsetOf0(X0,xD)
| ~ aSubsetOf0(xP,X0)
| ~ aSet0(xD) ),
inference(forward_subsumption_resolution,[status(thm)],[f4952,f145]) ).
fof(f5076,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xD)
| ~ aSet0(xD) ),
inference(resolution,[status(thm)],[f4953,f465]) ).
fof(f5480,plain,
! [X0] :
( ~ aSubsetOf0(X0,xD)
| ~ aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),X0)
| ~ aSet0(xD)
| ~ aSet0(X0)
| ~ aSet0(xD) ),
inference(resolution,[status(thm)],[f5076,f778]) ).
fof(f5481,plain,
! [X0] :
( ~ aSubsetOf0(X0,xD)
| ~ aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),X0)
| ~ aSet0(X0)
| ~ aSet0(xD) ),
inference(duplicate_literals_removal,[status(thm)],[f5480]) ).
fof(f5482,plain,
! [X0] :
( ~ aSubsetOf0(X0,xD)
| ~ aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),X0)
| ~ aSet0(xD) ),
inference(forward_subsumption_resolution,[status(thm)],[f5481,f145]) ).
fof(f7787,plain,
! [X0] :
( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))
| ~ isCountable0(sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f395,f398]) ).
fof(f7790,plain,
( ~ aSubsetOf0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),xD)
| ~ aSet0(xD)
| ~ isCountable0(sdtlpdtrp0(xN,xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f7787,f5482]) ).
fof(f7812,plain,
( ~ aSubsetOf0(xD,xD)
| ~ aSet0(xD)
| ~ isCountable0(sdtlpdtrp0(xN,xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f466,f7790]) ).
fof(f7813,plain,
( ~ aSubsetOf0(xD,xD)
| ~ aSet0(xD)
| ~ isCountable0(sdtlpdtrp0(xN,xn)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7812,f462]) ).
fof(f7863,plain,
( ~ aSet0(xD)
| ~ isCountable0(sdtlpdtrp0(xN,xn)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7813,f152]) ).
fof(f7864,plain,
( ~ aElementOf0(xn,szNzAzT0)
| ~ aSet0(xD) ),
inference(resolution,[status(thm)],[f7863,f399]) ).
fof(f7865,plain,
~ aSet0(xD),
inference(forward_subsumption_resolution,[status(thm)],[f7864,f462]) ).
fof(f7866,plain,
( ~ aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))
| ~ aSet0(sdtlpdtrp0(xN,xn)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1265,f7865]) ).
fof(f7867,plain,
( ~ aSet0(sdtlpdtrp0(xN,xn))
| sdtlpdtrp0(xN,xn) = slcrc0
| ~ aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)
| ~ aSet0(sdtlpdtrp0(xN,xn)) ),
inference(resolution,[status(thm)],[f7866,f2671]) ).
fof(f7869,plain,
( sdtlpdtrp0(xN,xn) = slcrc0
| ~ aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)
| ~ aSet0(sdtlpdtrp0(xN,xn)) ),
inference(duplicate_literals_removal,[status(thm)],[f7867]) ).
fof(f7870,plain,
( ~ aElementOf0(xn,szNzAzT0)
| sdtlpdtrp0(xN,xn) = slcrc0
| ~ aSet0(sdtlpdtrp0(xN,xn)) ),
inference(resolution,[status(thm)],[f7869,f398]) ).
fof(f7872,plain,
( ~ aElementOf0(xn,szNzAzT0)
| sdtlpdtrp0(xN,xn) = slcrc0 ),
inference(forward_subsumption_resolution,[status(thm)],[f7870,f2696]) ).
fof(f7879,plain,
sdtlpdtrp0(xN,xn) = slcrc0,
inference(forward_subsumption_resolution,[status(thm)],[f7872,f462]) ).
fof(f7901,plain,
( isCountable0(slcrc0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f7879,f399]) ).
fof(f8051,plain,
isCountable0(slcrc0),
inference(forward_subsumption_resolution,[status(thm)],[f7901,f462]) ).
fof(f8204,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8051,f571]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM629+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n004.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Mon Sep 21 02:45:39 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 34.08/9.99 % Refutation found
% 34.08/9.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 34.08/9.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.22/10.85 % Elapsed time: 5.460619 seconds
% 3.22/10.85 % CPU time: 37.445232 seconds
% 3.22/10.85 % Total memory used: 282.611 MB
% 3.22/10.85 % Net memory used: 256.987 MB
%------------------------------------------------------------------------------