%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM582+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 : 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:04 PM UTC 2026
% Result : Theorem 0.13s 0.60s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 46 ( 14 unt; 1 def)
% Number of atoms : 146 ( 5 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 174 ( 74 ~; 62 |; 26 &)
% ( 2 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-2 aty)
% Number of variables : 52 ( 50 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
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(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(sz00,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,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(f83,hypothesis,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W1,W0)
=> aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,conjecture,
aSubsetOf0(sdtlpdtrp0(xN,xi),xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
~ aSubsetOf0(sdtlpdtrp0(xN,xi),xS),
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f114,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(f115,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)],[f114]) ).
fof(f116,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)],[f115]) ).
fof(f117,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))],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f124,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f125,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f128,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(f129,plain,
! [X0,X1,X2] :
( aSubsetOf0(X0,X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X0,X1)
| ~ aSet0(X2)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f166,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f168,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f182,plain,
! [W0] :
( sdtlseqdt0(sz00,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f183,plain,
! [X0] :
( sdtlseqdt0(sz00,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f349,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f364,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(f367,plain,
sdtlpdtrp0(xN,sz00) = xS,
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f373,plain,
! [W0,W1] :
( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
| ~ sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f374,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f377,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f380,plain,
~ aSubsetOf0(sdtlpdtrp0(xN,xi),xS),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f428,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f349,f118]) ).
fof(f435,plain,
aSet0(xS),
inference(backward_subsumption_resolution,[status(thm)],[f428,f166]) ).
fof(f442,plain,
! [X0,X1,X2] :
( aSubsetOf0(X2,X1)
| ~ aSubsetOf0(X0,X1)
| ~ aSubsetOf0(X2,X0)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f129,f118]) ).
fof(f443,plain,
! [X0] :
( ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xi),X0)
| ~ aSet0(xS)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f442,f380]) ).
fof(f447,plain,
! [X0] :
( ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xi),X0)
| ~ aSet0(xS) ),
inference(forward_subsumption_resolution,[status(thm)],[f443,f118]) ).
fof(f500,plain,
! [X0] :
( ~ aSubsetOf0(X0,xS)
| ~ aSubsetOf0(sdtlpdtrp0(xN,xi),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f447,f435]) ).
fof(f522,plain,
! [X0] :
( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f374,f500]) ).
fof(f529,plain,
! [X0] :
( ~ aSubsetOf0(sdtlpdtrp0(xN,X0),xS)
| ~ sdtlseqdt0(X0,xi)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[status(thm)],[f522,f377]) ).
fof(f578,plain,
( ~ aSubsetOf0(xS,xS)
| ~ sdtlseqdt0(sz00,xi)
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f367,f529]) ).
fof(f580,plain,
( ~ aSubsetOf0(xS,xS)
| ~ sdtlseqdt0(sz00,xi) ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f168]) ).
fof(f630,plain,
( ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f183,f580]) ).
fof(f631,plain,
~ aSubsetOf0(xS,xS),
inference(forward_subsumption_resolution,[status(thm)],[f630,f377]) ).
fof(f633,plain,
~ aSet0(xS),
inference(resolution,[status(thm)],[f631,f125]) ).
fof(f635,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f633,f435]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM582+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.56 % Computer : n015.cluster.edu
% 0.08/0.56 % Model : x86_64 x86_64
% 0.08/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.56 % Memory : 8046.5625MB
% 0.08/0.56 % OS : Linux 6.8.0-71-generic
% 0.08/0.56 % CPULimit : 300
% 0.08/0.56 % WCLimit : 300
% 0.08/0.56 % DateTime : Mon Sep 21 02:45:21 UTC 2026
% 0.08/0.56 % CPUTime :
% 0.08/0.57 % Drodi V4.1.1
% 0.13/0.60 % Refutation found
% 0.13/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.62 % Elapsed time: 0.054989 seconds
% 0.13/0.62 % CPU time: 0.189374 seconds
% 0.13/0.62 % Total memory used: 110.533 MB
% 0.13/0.62 % Net memory used: 110.276 MB
%------------------------------------------------------------------------------