%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM625+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:14 PM UTC 2026
% Result : Theorem 0.13s 0.43s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 19
% Syntax : Number of formulae : 67 ( 21 unt; 9 def)
% Number of atoms : 220 ( 27 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 247 ( 94 ~; 90 |; 43 &)
% ( 15 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 7 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-3 aty)
% Number of variables : 84 ( 80 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
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(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
aSubsetOf0(xO,xS),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,hypothesis,
( xQ != slcrc0
& aSubsetOf0(xQ,xO) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
xp = szmzizndt0(xQ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,hypothesis,
( xP = sdtmndt0(xQ,szmzizndt0(xQ))
& aSet0(xP) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,hypothesis,
aElementOf0(xp,xQ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
aElementOf0(xx,xP),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
xp = xx,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f130,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f147,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(f148,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)],[f147]) ).
fof(f149,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)],[f148]) ).
fof(f150,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))],[f149]) ).
fof(f151,plain,
! [X0,X1] :
( aSet0(X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f176,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(f177,definition,
! [W0,W1,W3] :
( sP0_prd(W3,W1,W0)
<=> ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f178,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)],[f176,f177]) ).
fof(f179,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)],[f178]) ).
fof(f180,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)],[f179]) ).
fof(f181,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))],[f180]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( sP0_prd(X3,X1,X0)
| ~ aElementOf0(X3,X2)
| X2 != sdtmndt0(X0,X1)
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f199,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f382,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f452,plain,
aSubsetOf0(xO,xS),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f454,plain,
aSubsetOf0(xQ,xO),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f458,plain,
xp = szmzizndt0(xQ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f460,plain,
xP = sdtmndt0(xQ,szmzizndt0(xQ)),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f461,plain,
aElementOf0(xp,xQ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f471,plain,
aElementOf0(xx,xP),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f481,plain,
xp = xx,
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f482,plain,
! [W0,W1,W3] :
( ( W3 = W1
| ~ aElementOf0(W3,W0)
| ~ aElement0(W3)
| sP0_prd(W3,W1,W0) )
& ( ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) )
| ~ sP0_prd(W3,W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f177]) ).
fof(f483,plain,
( ! [W0,W1,W3] :
( W3 = W1
| ~ aElementOf0(W3,W0)
| ~ aElement0(W3)
| sP0_prd(W3,W1,W0) )
& ! [W0,W1,W3] :
( ( W3 != W1
& aElementOf0(W3,W0)
& aElement0(W3) )
| ~ sP0_prd(W3,W1,W0) ) ),
inference(miniscoping,[status(thm)],[f482]) ).
fof(f486,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f483]) ).
fof(f498,plain,
! [X0,X1,X2] :
( sP0_prd(X2,X1,X0)
| ~ aElementOf0(X2,sdtmndt0(X0,X1))
| ~ aElement0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f183]) ).
fof(f528,plain,
! [X0,X1] : ~ sP0_prd(X0,X0,X1),
inference(destructive_equality_resolution,[status(thm)],[f486]) ).
fof(f540,definition,
( sQ2_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( sQ2_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f547,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f199]) ).
fof(f548,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f547]) ).
fof(f604,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f151,f382]) ).
fof(f605,definition,
( sQ16_spl
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f608,plain,
( sQ16_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f604,f540,f605]) ).
fof(f624,plain,
( aSet0(xO)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f452,f151]) ).
fof(f625,definition,
( sQ19_spl
<=> aSet0(xO) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f628,plain,
( sQ19_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f624,f605,f625]) ).
fof(f629,plain,
( aSet0(xQ)
| ~ aSet0(xO) ),
inference(resolution,[status(thm)],[f454,f151]) ).
fof(f630,definition,
( sQ20_spl
<=> aSet0(xQ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f633,plain,
( sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f629,f625,f630]) ).
fof(f657,plain,
xx = szmzizndt0(xQ),
inference(forward_demodulation,[status(thm)],[f481,f458]) ).
fof(f658,plain,
aElementOf0(xx,xQ),
inference(forward_demodulation,[status(thm)],[f481,f461]) ).
fof(f660,plain,
( aElement0(xx)
| ~ aSet0(xQ) ),
inference(resolution,[status(thm)],[f658,f130]) ).
fof(f661,definition,
( sQ24_spl
<=> aElement0(xx) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f664,plain,
( sQ24_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f660,f630,f661]) ).
fof(f1120,plain,
xP = sdtmndt0(xQ,xx),
inference(forward_demodulation,[status(thm)],[f657,f460]) ).
fof(f1122,plain,
! [X0] :
( sP0_prd(X0,xx,xQ)
| ~ aElementOf0(X0,xP)
| ~ aElement0(xx)
| ~ aSet0(xQ) ),
inference(paramodulation,[status(thm)],[f1120,f498]) ).
fof(f1128,definition,
! [X0] :
( sQ90_spl
<=> ( sP0_prd(X0,xx,xQ)
| ~ aElementOf0(X0,xP) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1129,plain,
! [X0] :
( ~ sQ90_spl
| sP0_prd(X0,xx,xQ)
| ~ aElementOf0(X0,xP) ),
inference(component_clause,[status(thm)],[f1128]) ).
fof(f1131,plain,
( sQ90_spl
| ~ sQ24_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1122,f630,f661,f1128]) ).
fof(f1724,plain,
( ~ sQ90_spl
| ~ aElementOf0(xx,xP) ),
inference(resolution,[status(thm)],[f1129,f528]) ).
fof(f1729,plain,
( ~ sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1724,f471]) ).
fof(f1730,plain,
~ sQ90_spl,
inference(contradiction_clause,[status(thm)],[f1729]) ).
fof(f1731,plain,
$false,
inference(sat_refutation,[status(thm)],[f548,f608,f628,f633,f664,f1131,f1730]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM625+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n002.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 02:48:32 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.13/0.43 % Refutation found
% 0.13/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.47 % Elapsed time: 0.100385 seconds
% 0.13/0.47 % CPU time: 0.295595 seconds
% 0.13/0.47 % Total memory used: 68.609 MB
% 0.13/0.47 % Net memory used: 68.429 MB
%------------------------------------------------------------------------------