%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM633+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:16 PM UTC 2026
% Result : Theorem 0.10s 0.43s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 36 ( 6 unt; 2 def)
% Number of atoms : 295 ( 37 equ)
% Maximal formula atoms : 32 ( 8 avg)
% Number of connectives : 367 ( 108 ~; 99 |; 138 &)
% ( 3 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-2 aty)
% Number of variables : 90 ( 72 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f94,hypothesis,
( ! [W0] :
( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,hypothesis,
( isCountable0(xO)
& aSet0(xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
( aSubsetOf0(xO,xS)
& ! [W0] :
( aElementOf0(W0,xO)
=> aElementOf0(W0,xS) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,conjecture,
( ! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xO,xK))
| ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xO)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xO) )
& aSet0(W0) ) ) ) )
=> ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,szNzAzT0) )
& ~ ( W0 = slcrc0
| ~ ? [W1] : aElementOf0(W1,W0) ) ) )
=> ? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,xS) )
& aSet0(W1) ) ) )
& aElementOf0(W0,xT) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,negated_conjecture,
~ ( ! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xO,xK))
| ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xO)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xO) )
& aSet0(W0) ) ) ) )
=> ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xS) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,szNzAzT0) )
& ~ ( W0 = slcrc0
| ~ ? [W1] : aElementOf0(W1,W0) ) ) )
=> ? [W0] :
( ? [W1] :
( ! [W2] :
( ( aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W2)
=> aElementOf0(W3,W1) )
& aSet0(W2) )
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,xS) )
& aSet0(W1) ) ) )
& aElementOf0(W0,xT) ) ),
inference(negated_conjecture,[status(cth)],[f99]) ).
fof(f556,plain,
( ! [W0] :
( ( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
inference(NNF_transformation,[status(thm)],[f94]) ).
fof(f557,plain,
( ! [W0] :
( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(szDzizrdt0(xd),xT) ),
inference(miniscoping,[status(thm)],[f556]) ).
fof(f558,plain,
aElementOf0(szDzizrdt0(xd),xT),
inference(cnf_transformation,[status(thm)],[f557]) ).
fof(f576,plain,
isCountable0(xO),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f585,plain,
( aSubsetOf0(xO,xS)
& ! [W0] :
( aElementOf0(W0,xS)
| ~ aElementOf0(W0,xO) ) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f587,plain,
aSubsetOf0(xO,xS),
inference(cnf_transformation,[status(thm)],[f585]) ).
fof(f588,plain,
( ! [W0] :
( ! [W1] :
( ? [W2] :
( sdtlpdtrp0(xc,W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W1)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) )
| ~ aElementOf0(W0,xT) )
& ! [W0] :
( ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,W0) )
& W0 != slcrc0
& ? [W1] : aElementOf0(W1,W0) )
| ( ~ aElementOf0(W0,slbdtsldtrb0(xO,xK))
& ( sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xO)
& ( ? [W1] :
( ~ aElementOf0(W1,xO)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f589,definition,
! [W0] :
( sP10_prd(W0)
<=> ( ~ aElementOf0(W0,slbdtsldtrb0(xO,xK))
& ( sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xO)
& ( ? [W1] :
( ~ aElementOf0(W1,xO)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f590,definition,
! [W1] :
( sP11_prd(W1)
<=> ( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f591,plain,
( ! [W0] :
( ! [W1] :
( ? [W2] :
( sdtlpdtrp0(xc,W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xK))
& sbrdtbr0(W2) = xK
& aSubsetOf0(W2,W1)
& ! [W3] :
( aElementOf0(W3,W1)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| sP11_prd(W1) )
| ~ aElementOf0(W0,xT) )
& ! [W0] :
( ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,W0) )
& W0 != slcrc0
& ? [W1] : aElementOf0(W1,W0) )
| sP10_prd(W0) ) ),
inference(formula_renaming,[status(thm)],[f588,f590,f589]) ).
fof(f592,plain,
( ! [W0] :
( ! [W1] :
( ( sdtlpdtrp0(xc,sK37_skl(W1,W0)) != W0
& aElementOf0(sK37_skl(W1,W0),slbdtsldtrb0(W1,xK))
& sbrdtbr0(sK37_skl(W1,W0)) = xK
& aSubsetOf0(sK37_skl(W1,W0),W1)
& ! [W3] :
( aElementOf0(W3,W1)
| ~ aElementOf0(W3,sK37_skl(W1,W0)) )
& aSet0(sK37_skl(W1,W0)) )
| sP11_prd(W1) )
| ~ aElementOf0(W0,xT) )
& ! [W0] :
( ( sdtlpdtrp0(xc,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xc))
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,xS)
& ! [W1] :
( aElementOf0(W1,xS)
| ~ aElementOf0(W1,W0) )
& aSubsetOf0(W0,szNzAzT0)
& ! [W1] :
( aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W1,W0) )
& W0 != slcrc0
& aElementOf0(sK36_skl(W0),W0) )
| sP10_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl]),skolemize(W1,sK36_skl(W0)),skolemize(W2,sK37_skl(W1,W0))],[f591]) ).
fof(f602,plain,
! [X0] :
( sdtlpdtrp0(xc,X0) = szDzizrdt0(xd)
| sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f607,plain,
! [X0,X1] :
( aElementOf0(sK37_skl(X1,X0),slbdtsldtrb0(X1,xK))
| sP11_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f608,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,sK37_skl(X1,X0)) != X0
| sP11_prd(X1)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f737,plain,
! [W0] :
( ( aElementOf0(W0,slbdtsldtrb0(xO,xK))
| ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xO)
| ( ! [W1] :
( aElementOf0(W1,xO)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ) )
| sP10_prd(W0) )
& ( ( ~ aElementOf0(W0,slbdtsldtrb0(xO,xK))
& ( sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xO)
& ( ? [W1] :
( ~ aElementOf0(W1,xO)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) )
| ~ sP10_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f589]) ).
fof(f738,plain,
( ! [W0] :
( aElementOf0(W0,slbdtsldtrb0(xO,xK))
| ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xO)
| ( ! [W1] :
( aElementOf0(W1,xO)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ) )
| sP10_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,slbdtsldtrb0(xO,xK))
& ( sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xO)
& ( ? [W1] :
( ~ aElementOf0(W1,xO)
& aElementOf0(W1,W0) )
| ~ aSet0(W0) ) ) ) )
| ~ sP10_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f737]) ).
fof(f739,plain,
( ! [W0] :
( aElementOf0(W0,slbdtsldtrb0(xO,xK))
| ( sbrdtbr0(W0) = xK
& ( aSubsetOf0(W0,xO)
| ( ! [W1] :
( aElementOf0(W1,xO)
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ) )
| sP10_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,slbdtsldtrb0(xO,xK))
& ( sbrdtbr0(W0) != xK
| ( ~ aSubsetOf0(W0,xO)
& ( ( ~ aElementOf0(sK61_skl(W0),xO)
& aElementOf0(sK61_skl(W0),W0) )
| ~ aSet0(W0) ) ) ) )
| ~ sP10_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61_skl]),skolemize(W1,sK61_skl(W0))],[f738]) ).
fof(f743,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xO,xK))
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f739]) ).
fof(f747,plain,
! [W1] :
( ( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP11_prd(W1) )
& ( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) )
| ~ sP11_prd(W1) ) ),
inference(NNF_transformation,[status(thm)],[f590]) ).
fof(f748,plain,
( ! [W1] :
( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP11_prd(W1) )
& ! [W1] :
( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ? [W2] :
( ~ aElementOf0(W2,xS)
& aElementOf0(W2,W1) )
| ~ aSet0(W1) ) )
| ~ sP11_prd(W1) ) ),
inference(miniscoping,[status(thm)],[f747]) ).
fof(f749,plain,
( ! [W1] :
( ( isCountable0(W1)
& ( aSubsetOf0(W1,xS)
| ( ! [W2] :
( aElementOf0(W2,xS)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) ) )
| sP11_prd(W1) )
& ! [W1] :
( ~ isCountable0(W1)
| ( ~ aSubsetOf0(W1,xS)
& ( ( ~ aElementOf0(sK62_skl(W1),xS)
& aElementOf0(sK62_skl(W1),W1) )
| ~ aSet0(W1) ) )
| ~ sP11_prd(W1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl]),skolemize(W2,sK62_skl(W1))],[f748]) ).
fof(f752,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xS)
| ~ sP11_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f749]) ).
fof(f979,plain,
( ~ isCountable0(xO)
| ~ sP11_prd(xO) ),
inference(resolution,[status(thm)],[f752,f587]) ).
fof(f983,plain,
~ sP11_prd(xO),
inference(forward_subsumption_resolution,[status(thm)],[f979,f576]) ).
fof(f1432,plain,
! [X0] :
( ~ sP10_prd(sK37_skl(xO,X0))
| sP11_prd(xO)
| ~ aElementOf0(X0,xT) ),
inference(resolution,[status(thm)],[f607,f743]) ).
fof(f1440,plain,
! [X0] :
( ~ sP10_prd(sK37_skl(xO,X0))
| ~ aElementOf0(X0,xT) ),
inference(forward_subsumption_resolution,[status(thm)],[f1432,f983]) ).
fof(f1522,plain,
! [X0] :
( sP10_prd(sK37_skl(X0,szDzizrdt0(xd)))
| sP11_prd(X0)
| ~ aElementOf0(szDzizrdt0(xd),xT) ),
inference(resolution,[status(thm)],[f608,f602]) ).
fof(f1524,plain,
! [X0] :
( sP10_prd(sK37_skl(X0,szDzizrdt0(xd)))
| sP11_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1522,f558]) ).
fof(f1535,plain,
( ~ aElementOf0(szDzizrdt0(xd),xT)
| sP11_prd(xO) ),
inference(resolution,[status(thm)],[f1524,f1440]) ).
fof(f1536,plain,
~ aElementOf0(szDzizrdt0(xd),xT),
inference(forward_subsumption_resolution,[status(thm)],[f1535,f983]) ).
fof(f1556,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1536,f558]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM633+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:49:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.43 % Refutation found
% 0.10/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.47 % Elapsed time: 0.092824 seconds
% 0.10/0.47 % CPU time: 0.372301 seconds
% 0.10/0.47 % Total memory used: 128.901 MB
% 0.10/0.47 % Net memory used: 128.330 MB
%------------------------------------------------------------------------------