%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM566+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 : n019.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:01 PM UTC 2026
% Result : Theorem 10.26s 2.01s
% Output : CNFRefutation 6.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 57 ( 17 unt; 1 def)
% Number of atoms : 160 ( 14 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 183 ( 80 ~; 69 |; 24 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 61 ( 54 !; 7 ?)
% 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(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aElementOf0(W1,szDzozmdt0(W0))
=> aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,hypothesis,
( isFinite0(xT)
& aSet0(xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,hypothesis,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aFunction0(xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,hypothesis,
xK = sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,hypothesis,
aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
! [W0] :
( aElementOf0(W0,slbdtsldtrb0(xS,sz00))
=> sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,conjecture,
? [W0] :
( ? [W1] :
( ! [W2] :
( aElementOf0(W2,slbdtsldtrb0(W1,xK))
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& aSubsetOf0(W1,xS) )
& aElementOf0(W0,xT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,negated_conjecture,
~ ? [W0] :
( ? [W1] :
( ! [W2] :
( aElementOf0(W2,slbdtsldtrb0(W1,xK))
=> sdtlpdtrp0(xc,W2) = W0 )
& isCountable0(W1)
& aSubsetOf0(W1,xS) )
& aElementOf0(W0,xT) ),
inference(negated_conjecture,[status(cth)],[f81]) ).
fof(f107,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(f108,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)],[f107]) ).
fof(f109,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)],[f108]) ).
fof(f110,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))],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f117,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f118,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f159,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f319,plain,
! [W0] :
( ! [W1] :
( aElementOf0(sdtlpdtrp0(W0,W1),sdtlcdtrc0(W0,szDzozmdt0(W0)))
| ~ aElementOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f320,plain,
! [X0,X1] :
( aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0)))
| ~ aElementOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f339,plain,
aSet0(xT),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f342,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f343,plain,
isCountable0(xS),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f344,plain,
aFunction0(xc),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f345,plain,
szDzozmdt0(xc) = slbdtsldtrb0(xS,xK),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f346,plain,
aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f353,plain,
xK = sz00,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f354,plain,
aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f355,plain,
! [W0] :
( sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0)
| ~ aElementOf0(W0,slbdtsldtrb0(xS,sz00)) ),
inference(pre_NNF_transformation,[status(thm)],[f80]) ).
fof(f356,plain,
! [X0] :
( sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0)
| ~ aElementOf0(X0,slbdtsldtrb0(xS,sz00)) ),
inference(cnf_transformation,[status(thm)],[f355]) ).
fof(f357,plain,
! [W0] :
( ! [W1] :
( ? [W2] :
( sdtlpdtrp0(xc,W2) != W0
& aElementOf0(W2,slbdtsldtrb0(W1,xK)) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,xS) )
| ~ aElementOf0(W0,xT) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f358,plain,
! [W0] :
( ! [W1] :
( ( sdtlpdtrp0(xc,sK21_skl(W1,W0)) != W0
& aElementOf0(sK21_skl(W1,W0),slbdtsldtrb0(W1,xK)) )
| ~ isCountable0(W1)
| ~ aSubsetOf0(W1,xS) )
| ~ aElementOf0(W0,xT) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W2,sK21_skl(W1,W0))],[f357]) ).
fof(f359,plain,
! [X0,X1] :
( aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,xK))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f360,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,sK21_skl(X1,X0)) != X0
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f412,plain,
! [X0,X1] :
( aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,sz00))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| ~ aElementOf0(X0,xT) ),
inference(backward_demodulation,[status(thm)],[f353,f359]) ).
fof(f414,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f111,f342]) ).
fof(f416,plain,
szDzozmdt0(xc) = slbdtsldtrb0(xS,sz00),
inference(forward_demodulation,[status(thm)],[f353,f345]) ).
fof(f417,plain,
aElementOf0(slcrc0,szDzozmdt0(xc)),
inference(forward_demodulation,[status(thm)],[f416,f354]) ).
fof(f426,plain,
aSet0(xS),
inference(backward_subsumption_resolution,[status(thm)],[f414,f159]) ).
fof(f444,plain,
! [X0] :
( aElementOf0(sK21_skl(xS,X0),szDzozmdt0(xc))
| ~ isCountable0(xS)
| ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(X0,xT) ),
inference(paramodulation,[status(thm)],[f416,f412]) ).
fof(f445,plain,
! [X0] :
( aElementOf0(sK21_skl(xS,X0),szDzozmdt0(xc))
| ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(X0,xT) ),
inference(forward_subsumption_resolution,[status(thm)],[f444,f343]) ).
fof(f456,plain,
! [X0] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aSet0(xT) ),
inference(resolution,[status(thm)],[f346,f112]) ).
fof(f460,plain,
! [X0] :
( aElementOf0(X0,xT)
| ~ aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) ),
inference(forward_subsumption_resolution,[status(thm)],[f456,f339]) ).
fof(f606,plain,
! [X0] :
( sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0)
| ~ aElementOf0(X0,szDzozmdt0(xc)) ),
inference(forward_demodulation,[status(thm)],[f416,f356]) ).
fof(f607,plain,
! [X0] :
( ~ isCountable0(X0)
| ~ aSubsetOf0(X0,xS)
| ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ aElementOf0(sK21_skl(X0,sdtlpdtrp0(xc,slcrc0)),szDzozmdt0(xc)) ),
inference(resolution,[status(thm)],[f606,f360]) ).
fof(f672,plain,
( ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ isCountable0(xS)
| ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),xT) ),
inference(resolution,[status(thm)],[f607,f445]) ).
fof(f673,plain,
( ~ isCountable0(xS)
| ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),xT) ),
inference(duplicate_literals_removal,[status(thm)],[f672]) ).
fof(f674,plain,
( ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),xT) ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f343]) ).
fof(f2650,plain,
! [X0] :
( aElementOf0(sdtlpdtrp0(xc,X0),xT)
| ~ aElementOf0(X0,szDzozmdt0(xc))
| ~ aFunction0(xc) ),
inference(resolution,[status(thm)],[f320,f460]) ).
fof(f2653,plain,
! [X0] :
( aElementOf0(sdtlpdtrp0(xc,X0),xT)
| ~ aElementOf0(X0,szDzozmdt0(xc)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2650,f344]) ).
fof(f2654,plain,
( ~ aSubsetOf0(xS,xS)
| ~ aElementOf0(slcrc0,szDzozmdt0(xc)) ),
inference(resolution,[status(thm)],[f2653,f674]) ).
fof(f2656,plain,
~ aSubsetOf0(xS,xS),
inference(forward_subsumption_resolution,[status(thm)],[f2654,f417]) ).
fof(f2658,plain,
~ aSet0(xS),
inference(resolution,[status(thm)],[f2656,f118]) ).
fof(f2659,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2658,f426]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM566+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n019.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.57 % DateTime : Mon Sep 21 02:40:21 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.13/0.58 % Drodi V4.1.1
% 10.26/2.01 % Refutation found
% 10.26/2.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.26/2.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.19/2.04 % Elapsed time: 1.459047 seconds
% 6.19/2.04 % CPU time: 11.160400 seconds
% 6.19/2.04 % Total memory used: 184.159 MB
% 6.19/2.04 % Net memory used: 176.219 MB
%------------------------------------------------------------------------------